Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > fh1 | Unicode version |
Description: Foulis-Holland Theorem. |
Ref | Expression |
---|---|
fh.1 | |
fh.2 |
Ref | Expression |
---|---|
fh1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ledi 174 | . . 3 | |
2 | ancom 74 | . . . . . 6 | |
3 | df-a 40 | . . . . . . . . 9 | |
4 | df-a 40 | . . . . . . . . 9 | |
5 | 3, 4 | 2or 72 | . . . . . . . 8 |
6 | df-a 40 | . . . . . . . . . 10 | |
7 | 6 | ax-r1 35 | . . . . . . . . 9 |
8 | 7 | con3 68 | . . . . . . . 8 |
9 | 5, 8 | ax-r2 36 | . . . . . . 7 |
10 | 9 | con2 67 | . . . . . 6 |
11 | 2, 10 | 2an 79 | . . . . 5 |
12 | anass 76 | . . . . . . 7 | |
13 | fh.1 | . . . . . . . . . . . 12 | |
14 | 13 | comcom2 183 | . . . . . . . . . . 11 |
15 | 14 | com3ii 457 | . . . . . . . . . 10 |
16 | fh.2 | . . . . . . . . . . . 12 | |
17 | 16 | comcom2 183 | . . . . . . . . . . 11 |
18 | 17 | com3ii 457 | . . . . . . . . . 10 |
19 | 15, 18 | 2an 79 | . . . . . . . . 9 |
20 | anandi 114 | . . . . . . . . 9 | |
21 | anandi 114 | . . . . . . . . 9 | |
22 | 19, 20, 21 | 3tr1 63 | . . . . . . . 8 |
23 | 22 | lan 77 | . . . . . . 7 |
24 | 12, 23 | ax-r2 36 | . . . . . 6 |
25 | an12 81 | . . . . . 6 | |
26 | 24, 25 | ax-r2 36 | . . . . 5 |
27 | 11, 26 | ax-r2 36 | . . . 4 |
28 | oran 87 | . . . . . . . . . 10 | |
29 | 28 | ax-r1 35 | . . . . . . . . 9 |
30 | 29 | con3 68 | . . . . . . . 8 |
31 | 30 | lan 77 | . . . . . . 7 |
32 | dff 101 | . . . . . . . 8 | |
33 | 32 | ax-r1 35 | . . . . . . 7 |
34 | 31, 33 | ax-r2 36 | . . . . . 6 |
35 | 34 | lan 77 | . . . . 5 |
36 | an0 108 | . . . . 5 | |
37 | 35, 36 | ax-r2 36 | . . . 4 |
38 | 27, 37 | ax-r2 36 | . . 3 |
39 | 1, 38 | oml3 452 | . 2 |
40 | 39 | ax-r1 35 | 1 |
Colors of variables: term |
Syntax hints: wb 1 wc 3 wn 4 wo 6 wa 7 wf 9 |
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-r3 439 |
This theorem depends on definitions: df-b 39 df-a 40 df-t 41 df-f 42 df-le1 130 df-le2 131 df-c1 132 df-c2 133 |
This theorem is referenced by: fh3 471 fh1r 473 com2or 483 nbdi 486 oml4 487 gsth 489 i3bi 496 dfi3b 499 i3lem1 504 lem4 511 i3abs3 524 i3orlem7 558 i3orlem8 559 ud3lem1b 567 ud4lem1a 577 ud4lem1d 580 u5lemaa 604 u3lemc4 703 u4lemle2 718 u5lemle2 719 u5lembi 725 u12lembi 726 u24lem 770 u3lem13a 789 bi1o1a 798 3vded21 817 3vded3 819 comanblem2 871 mhlem1 877 mlaconjolem 885 lem4.6.2e1 1080 |
Copyright terms: Public domain | W3C validator |