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

Theorem wr1 197
Description: Weak R1.
Hypothesis
Ref Expression
wr1.1 (a == b) = 1
Assertion
Ref Expression
wr1 (b == a) = 1

Proof of Theorem wr1
StepHypRef Expression
1 bicom 96 . 2 (b == a) = (a == b)
2 wr1.1 . 2 (a == b) = 1
31, 2ax-r2 36 1 (b == a) = 1
Colors of variables: term
Syntax hints:   = wb 1   == tb 5  1wt 8
This theorem is referenced by:  wwbmpr  206  wr2  371  w3tr1  374  w3tr2  375  wleoa  376  wleao  377  wom5  381  wcomlem  382  wleror  393  wleran  394  wletr  396  wlbtr  398  wle3tr1  399  wle3tr2  400  wlebi  402  wledi  405  wledio  406  wlecom  409  wcomd  418  wcom3ii  419  wfh1  423  wfh2  424  wfh3  425  wfh4  426  wcom2or  427  wlem14  430  woml6  436  wdid0id5  1109  wdid0id1  1110  wdid0id2  1111  wdid0id3  1112  wdid0id4  1113
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
  Copyright terms: Public domain W3C validator