Quantum Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > QLE Home > Th. List > comanr1 | GIF version |
Description: Commutation law. (Contributed by NM, 26-Nov-1997.) |
Ref | Expression |
---|---|
comanr1 | a C (a ∩ b) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coman1 185 | . 2 (a ∩ b) C a | |
2 | 1 | comcom 453 | 1 a C (a ∩ b) |
Colors of variables: term |
Syntax hints: C wc 3 ∩ 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: combi 485 ud3lem1a 566 ud5lem3a 591 ud5lem3b 592 ud5lem3 594 u1lemaa 600 u3lemaa 602 u4lemaa 603 u5lemaa 604 u3lemana 607 u4lemana 608 u5lemana 609 u1lemc1 680 u5lemc1 684 u4lemle2 718 u5lemle2 719 u21lembi 727 u4lem1 737 u4lem4 759 u24lem 770 u1lem11 780 u3lem10 785 u3lem13a 789 u3lem13b 790 bi1o1a 798 i1abs 801 3vth9 812 mlalem 832 bi3 839 bi4 840 imp3 841 mlaconj4 844 comanblem1 870 comanblem2 871 oas 925 |
Copyright terms: Public domain | W3C validator |