Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > fh4 | Unicode version |
Description: Foulis-Holland Theorem. |
Ref | Expression |
---|---|
fh.1 | |
fh.2 |
Ref | Expression |
---|---|
fh4 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fh.1 | . . . . 5 | |
2 | 1 | comcom4 455 | . . . 4 |
3 | fh.2 | . . . . 5 | |
4 | 3 | comcom4 455 | . . . 4 |
5 | 2, 4 | fh2 470 | . . 3 |
6 | anor2 89 | . . . 4 | |
7 | df-a 40 | . . . . . . 7 | |
8 | 7 | ax-r1 35 | . . . . . 6 |
9 | 8 | lor 70 | . . . . 5 |
10 | 9 | ax-r4 37 | . . . 4 |
11 | 6, 10 | ax-r2 36 | . . 3 |
12 | oran 87 | . . . 4 | |
13 | oran 87 | . . . . . . 7 | |
14 | oran 87 | . . . . . . 7 | |
15 | 13, 14 | 2an 79 | . . . . . 6 |
16 | 15 | ax-r1 35 | . . . . 5 |
17 | 16 | ax-r4 37 | . . . 4 |
18 | 12, 17 | ax-r2 36 | . . 3 |
19 | 5, 11, 18 | 3tr2 64 | . 2 |
20 | 19 | con1 66 | 1 |
Colors of variables: term |
Syntax hints: wb 1 wc 3 wn 4 wo 6 wa 7 |
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: fh4r 476 fh4c 478 df2i3 498 i3abs3 524 i3con 551 ud3lem1c 568 ud4lem1c 579 ud4lem1 581 ud5lem1 589 ud5lem3 594 u5lemaa 604 u4lemona 628 u3lemob 632 u3lemonb 637 u1lemc4 701 u2lemc4 702 u3lemc4 703 u4lemc4 704 u5lemc4 705 u4lem1 737 u2lem3 750 u1lem4 757 u4lem5 764 u5lem5 765 u4lem6 768 u5lem6 769 u3lem11 786 orbi 842 e2ast2 894 |
Copyright terms: Public domain | W3C validator |