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

Theorem bicom 96
 Description: Commutative law. (Contributed by NM, 10-Aug-1997.)
Assertion
Ref Expression
bicom (ab) = (ba)

Proof of Theorem bicom
StepHypRef Expression
1 ancom 74 . . 3 (ab) = (ba)
2 ancom 74 . . 3 (ab ) = (ba )
31, 22or 72 . 2 ((ab) ∪ (ab )) = ((ba) ∪ (ba ))
4 dfb 94 . 2 (ab) = ((ab) ∪ (ab ))
5 dfb 94 . 2 (ba) = ((ba) ∪ (ba ))
63, 4, 53tr1 63 1 (ab) = (ba)
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38 This theorem depends on definitions:  df-b 39  df-a 40 This theorem is referenced by:  rbi  98  wr1  197  wwfh1  216  wwfh2  217  ska12  240  nomcon5  306  nom35  324  nom55  336  nom65  342  ka4ot  435  ublemc2  729  mlaconj4  844  distid  887  oago3.29  889  oago3.21x  890
 Copyright terms: Public domain W3C validator