Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > wr5-2v | Unicode version |
Description: WOML derived from 2-variable axioms. |
Ref | Expression |
---|---|
wr5-2v.1 |
Ref | Expression |
---|---|
wr5-2v |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-i2 45 | . . 3 | |
2 | df-i2 45 | . . . . 5 | |
3 | 2 | ax-r1 35 | . . . 4 |
4 | anandir 115 | . . . . . 6 | |
5 | anass 76 | . . . . . . 7 | |
6 | anor3 90 | . . . . . . . 8 | |
7 | 6 | lan 77 | . . . . . . 7 |
8 | 5, 7 | ax-r2 36 | . . . . . 6 |
9 | anor3 90 | . . . . . . 7 | |
10 | 9, 6 | 2an 79 | . . . . . 6 |
11 | 4, 8, 10 | 3tr2 64 | . . . . 5 |
12 | 11 | lor 70 | . . . 4 |
13 | df-i1 44 | . . . . . 6 | |
14 | wr5-2v.1 | . . . . . . . . . . . . . 14 | |
15 | wlem1 243 | . . . . . . . . . . . . . 14 | |
16 | 14, 15 | skr0 242 | . . . . . . . . . . . . 13 |
17 | 16 | ax-r1 35 | . . . . . . . . . . . 12 |
18 | lea 160 | . . . . . . . . . . . 12 | |
19 | 17, 18 | bltr 138 | . . . . . . . . . . 11 |
20 | le1 146 | . . . . . . . . . . 11 | |
21 | 19, 20 | lebi 145 | . . . . . . . . . 10 |
22 | df-i1 44 | . . . . . . . . . 10 | |
23 | 21, 22 | ax-r2 36 | . . . . . . . . 9 |
24 | leo 158 | . . . . . . . . . . 11 | |
25 | 24 | lelan 167 | . . . . . . . . . 10 |
26 | 25 | lelor 166 | . . . . . . . . 9 |
27 | 23, 26 | bltr 138 | . . . . . . . 8 |
28 | le1 146 | . . . . . . . 8 | |
29 | 27, 28 | lebi 145 | . . . . . . 7 |
30 | 29 | ax-r1 35 | . . . . . 6 |
31 | 13, 30 | ax-r2 36 | . . . . 5 |
32 | 31 | 2vwomr1a 363 | . . . 4 |
33 | 3, 12, 32 | 3tr2 64 | . . 3 |
34 | 1, 33 | ax-r2 36 | . 2 |
35 | df-i2 45 | . . 3 | |
36 | df-i2 45 | . . . . 5 | |
37 | 36 | ax-r1 35 | . . . 4 |
38 | anandir 115 | . . . . . 6 | |
39 | anass 76 | . . . . . . 7 | |
40 | 9 | lan 77 | . . . . . . 7 |
41 | 39, 40 | ax-r2 36 | . . . . . 6 |
42 | 6, 9 | 2an 79 | . . . . . 6 |
43 | 38, 41, 42 | 3tr2 64 | . . . . 5 |
44 | 43 | lor 70 | . . . 4 |
45 | df-i1 44 | . . . . . 6 | |
46 | lear 161 | . . . . . . . . . . . 12 | |
47 | 17, 46 | bltr 138 | . . . . . . . . . . 11 |
48 | le1 146 | . . . . . . . . . . 11 | |
49 | 47, 48 | lebi 145 | . . . . . . . . . 10 |
50 | df-i1 44 | . . . . . . . . . 10 | |
51 | 49, 50 | ax-r2 36 | . . . . . . . . 9 |
52 | leo 158 | . . . . . . . . . . 11 | |
53 | 52 | lelan 167 | . . . . . . . . . 10 |
54 | 53 | lelor 166 | . . . . . . . . 9 |
55 | 51, 54 | bltr 138 | . . . . . . . 8 |
56 | le1 146 | . . . . . . . 8 | |
57 | 55, 56 | lebi 145 | . . . . . . 7 |
58 | 57 | ax-r1 35 | . . . . . 6 |
59 | 45, 58 | ax-r2 36 | . . . . 5 |
60 | 59 | 2vwomr1a 363 | . . . 4 |
61 | 37, 44, 60 | 3tr2 64 | . . 3 |
62 | 35, 61 | ax-r2 36 | . 2 |
63 | 34, 62 | 2vwomlem 365 | 1 |
Colors of variables: term |
Syntax hints: wb 1 wn 4 tb 5 wo 6 wa 7 wt 8 wi1 12 wi2 13 |
This theorem was proved from axioms: ax-a1 30 ax-a2 31 ax-a3 32 ax-a4 33 ax-a5 34 ax-r1 35 ax-r2 36 ax-r4 37 ax-r5 38 ax-wom 361 |
This theorem depends on definitions: df-b 39 df-a 40 df-t 41 df-f 42 df-i1 44 df-i2 45 df-le1 130 df-le2 131 |
This theorem is referenced by: wom3 367 wlor 368 wran 369 wr2 371 w2or 372 wler 391 wleror 393 wletr 396 wbltr 397 wbile 401 wlecom 409 wcomcom2 415 wfh2 424 wr5 431 ska2 432 woml6 436 woml7 437 |
Copyright terms: Public domain | W3C validator |