Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > comcom | Unicode version |
Description: Commutation is symmetric. Kalmbach 83 p. 22. |
Ref | Expression |
---|---|
comcom.1 |
Ref | Expression |
---|---|
comcom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-a2 31 | . . . . . . . . . 10 | |
2 | 1 | ran 78 | . . . . . . . . 9 |
3 | ancom 74 | . . . . . . . . 9 | |
4 | 2, 3 | ax-r2 36 | . . . . . . . 8 |
5 | anabs 121 | . . . . . . . 8 | |
6 | 4, 5 | ax-r2 36 | . . . . . . 7 |
7 | 6 | lan 77 | . . . . . 6 |
8 | comcom.1 | . . . . . . . . . . . 12 | |
9 | 8 | df-c2 133 | . . . . . . . . . . 11 |
10 | df-a 40 | . . . . . . . . . . . 12 | |
11 | anor1 88 | . . . . . . . . . . . 12 | |
12 | 10, 11 | 2or 72 | . . . . . . . . . . 11 |
13 | 9, 12 | ax-r2 36 | . . . . . . . . . 10 |
14 | 13 | ax-r4 37 | . . . . . . . . 9 |
15 | df-a 40 | . . . . . . . . . 10 | |
16 | 15 | ax-r1 35 | . . . . . . . . 9 |
17 | 14, 16 | ax-r2 36 | . . . . . . . 8 |
18 | 17 | ran 78 | . . . . . . 7 |
19 | anass 76 | . . . . . . 7 | |
20 | 18, 19 | ax-r2 36 | . . . . . 6 |
21 | 10 | con2 67 | . . . . . . 7 |
22 | 21 | ran 78 | . . . . . 6 |
23 | 7, 20, 22 | 3tr1 63 | . . . . 5 |
24 | 23 | lor 70 | . . . 4 |
25 | 24 | ax-r1 35 | . . 3 |
26 | ax-a2 31 | . . . . . 6 | |
27 | ancom 74 | . . . . . . . 8 | |
28 | 27 | lor 70 | . . . . . . 7 |
29 | orabs 120 | . . . . . . 7 | |
30 | 28, 29 | ax-r2 36 | . . . . . 6 |
31 | 26, 30 | ax-r2 36 | . . . . 5 |
32 | 31 | df-le1 130 | . . . 4 |
33 | 32 | oml2 451 | . . 3 |
34 | ancom 74 | . . . 4 | |
35 | 27, 34 | 2or 72 | . . 3 |
36 | 25, 33, 35 | 3tr2 64 | . 2 |
37 | 36 | df-c1 132 | 1 |
Colors of variables: term |
Syntax hints: wc 3 wn 4 wo 6 wa 7 |
This theorem was proved from axioms: ax-a1 30 ax-a2 31 ax-a3 32 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: comcom3 454 com3ii 457 comor1 461 comorr2 463 comanr1 464 comanr2 465 fh2 470 com2or 483 nbdi 486 oml4 487 gsth 489 gsth2 490 gt1 492 i3bi 496 df2i3 498 i3lem1 504 comi31 508 lem4 511 i3abs3 524 i3con 551 ud1lem1 560 ud1lem3 562 ud2lem3 565 ud3lem1a 566 ud3lem1c 568 ud3lem3 576 ud4lem1a 577 ud4lem1b 578 ud4lem1c 579 ud4lem1 581 ud4lem3 585 ud5lem1a 586 ud5lem1 589 u4lemaa 603 u4lemana 608 u3lemab 612 u3lemanb 617 comi12 707 i1com 708 comi1 709 u4lemle2 718 u5lembi 725 u12lembi 726 u1lem1 734 u3lem1 736 u5lem1 738 u3lem2 746 u4lem2 747 u5lem2 748 u4lem4 759 u5lem5 765 u5lem6 769 u1lem8 776 u1lem11 780 u3lem13b 790 u3lem15 795 bi1o1a 798 test 802 3vcom 813 3vded21 817 3vded3 819 2oalem1 825 bi3 839 bi4 840 orbi 842 negantlem2 849 elimcons 868 comanblem1 870 mhlem 876 mhlem1 877 marsdenlem1 880 marsdenlem2 881 marsdenlem3 882 mh2 884 mlaconjolem 885 mhcor1 888 e2ast2 894 e2astlem1 895 govar 896 oau 929 oa23 936 oacom 1011 oacom3 1013 oa3moa3 1029 lem4.6.2e1 1080 lem4.6.6i1j3 1092 |
Copyright terms: Public domain | W3C validator |