QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  comcom5 GIF version

Theorem comcom5 458
Description: Commutation equivalence. Kalmbach 83 p. 23. (Contributed by NM, 27-Aug-1997.)
Hypothesis
Ref Expression
comcom5.1 a C b
Assertion
Ref Expression
comcom5 a C b

Proof of Theorem comcom5
StepHypRef Expression
1 comcom5.1 . . . . 5 a C b
21comcom4 455 . . . 4 a C b
32df-c2 133 . . 3 a = ((a b ) ∪ (a b ))
4 ax-a1 30 . . 3 a = a
5 ax-a1 30 . . . . 5 b = b
64, 52an 79 . . . 4 (ab) = (a b )
7 ax-a1 30 . . . . 5 b = b
84, 72an 79 . . . 4 (ab ) = (a b )
96, 82or 72 . . 3 ((ab) ∪ (ab )) = ((a b ) ∪ (a b ))
103, 4, 93tr1 63 . 2 a = ((ab) ∪ (ab ))
1110df-c1 132 1 a C b
Colors of variables: term
Syntax hints:   C 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:  comcom6  459  comcom7  460  comdr  466  df2c1  468  com2an  484  oml4  487  gstho  491  df2i3  498  i3lem2  505  comi31  508  ud1lem1  560  ud1lem3  562  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1d  580  ud4lem1  581  ud5lem1a  586
  Copyright terms: Public domain W3C validator