Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > fh2 | Unicode version |
Description: Foulis-Holland Theorem. |
Ref | Expression |
---|---|
fh.1 | |
fh.2 |
Ref | Expression |
---|---|
fh2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ledi 174 | . . 3 | |
2 | oran 87 | . . . . . . . . . . 11 | |
3 | df-a 40 | . . . . . . . . . . . . . 14 | |
4 | 3 | con2 67 | . . . . . . . . . . . . 13 |
5 | 4 | ran 78 | . . . . . . . . . . . 12 |
6 | 5 | ax-r4 37 | . . . . . . . . . . 11 |
7 | 2, 6 | ax-r2 36 | . . . . . . . . . 10 |
8 | 7 | con2 67 | . . . . . . . . 9 |
9 | 8 | lan 77 | . . . . . . . 8 |
10 | an4 86 | . . . . . . . . 9 | |
11 | fh.1 | . . . . . . . . . . . . . 14 | |
12 | 11 | comcom 453 | . . . . . . . . . . . . 13 |
13 | 12 | comcom2 183 | . . . . . . . . . . . 12 |
14 | 13 | com3ii 457 | . . . . . . . . . . 11 |
15 | ancom 74 | . . . . . . . . . . 11 | |
16 | 14, 15 | ax-r2 36 | . . . . . . . . . 10 |
17 | 16 | ran 78 | . . . . . . . . 9 |
18 | 10, 17 | ax-r2 36 | . . . . . . . 8 |
19 | 9, 18 | ax-r2 36 | . . . . . . 7 |
20 | an4 86 | . . . . . . 7 | |
21 | 19, 20 | ax-r2 36 | . . . . . 6 |
22 | ax-a1 30 | . . . . . . . . . 10 | |
23 | 22 | ax-r5 38 | . . . . . . . . 9 |
24 | 23 | lan 77 | . . . . . . . 8 |
25 | fh.2 | . . . . . . . . . 10 | |
26 | 25 | comcom3 454 | . . . . . . . . 9 |
27 | 26 | com3ii 457 | . . . . . . . 8 |
28 | 24, 27 | ax-r2 36 | . . . . . . 7 |
29 | 28 | ran 78 | . . . . . 6 |
30 | 21, 29 | ax-r2 36 | . . . . 5 |
31 | anass 76 | . . . . 5 | |
32 | 30, 31 | ax-r2 36 | . . . 4 |
33 | anass 76 | . . . . . . . 8 | |
34 | 33 | ax-r1 35 | . . . . . . 7 |
35 | an12 81 | . . . . . . 7 | |
36 | dff 101 | . . . . . . 7 | |
37 | 34, 35, 36 | 3tr1 63 | . . . . . 6 |
38 | 37 | lan 77 | . . . . 5 |
39 | an0 108 | . . . . 5 | |
40 | 38, 39 | ax-r2 36 | . . . 4 |
41 | 32, 40 | ax-r2 36 | . . 3 |
42 | 1, 41 | oml3 452 | . 2 |
43 | 42 | 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: fh4 472 fh2r 474 fh2c 477 i3bi 496 ud3lem1a 566 ud4lem1a 577 ud4lem1b 578 ud5lem1a 586 ud5lem1b 587 ud5lem3a 591 ud5lem3b 592 u1lemle2 715 u2lemle2 716 u4lemle2 718 u21lembi 727 u1lem4 757 u4lem6 768 u3lem11 786 u3lem13b 790 2oath1 826 oale 829 mlalem 832 bi3 839 bi4 840 imp3 841 elimcons 868 mhlemlem1 874 mhlem 876 marsdenlem2 881 e2astlem1 895 oas 925 |
Copyright terms: Public domain | W3C validator |