QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  bicom Unicode version
Theorem bicom 96
Description: Commutative law.
Assertion
Ref Expression
bicom (a == b) = (b == a)
Proof of Theorem bicom
StepHypRef Expression
1 ancom 74 . . 3 (a ^ b) = (b ^ a)
2 ancom 74 . . 3 (a' ^ b') = (b' ^ a')
31, 22or 72 . 2 ((a ^ b) v (a' ^ b')) = ((b ^ a) v (b' ^ a'))
4 dfb 94 . 2 (a == b) = ((a ^ b) v (a' ^ b'))
5 dfb 94 . 2 (b == a) = ((b ^ a) v (b' ^ a'))
63, 4, 53tr1 63 1 (a == b) = (b == a)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v 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