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

Theorem wr2 371
Description: Inference rule of AUQL.
Hypotheses
Ref Expression
wr2.1 (a == b) = 1
wr2.2 (b == c) = 1
Assertion
Ref Expression
wr2 (a == c) = 1

Proof of Theorem wr2
StepHypRef Expression
1 wr2.2 . . 3 (b == c) = 1
2 dfb 94 . . . . 5 (b == c) = ((b ^ c) v (b' ^ c'))
32rbi 98 . . . 4 ((b == c) == ((a ^ c) v (b' ^ c'))) = (((b ^ c) v (b' ^ c')) == ((a ^ c) v (b' ^ c')))
4 wr2.1 . . . . . . 7 (a == b) = 1
54wr1 197 . . . . . 6 (b == a) = 1
65wran 369 . . . . 5 ((b ^ c) == (a ^ c)) = 1
76wr5-2v 366 . . . 4 (((b ^ c) v (b' ^ c')) == ((a ^ c) v (b' ^ c'))) = 1
83, 7ax-r2 36 . . 3 ((b == c) == ((a ^ c) v (b' ^ c'))) = 1
91, 8wwbmp 205 . 2 ((a ^ c) v (b' ^ c')) = 1
10 dfb 94 . . . 4 (a == c) = ((a ^ c) v (a' ^ c'))
1110rbi 98 . . 3 ((a == c) == ((a ^ c) v (b' ^ c'))) = (((a ^ c) v (a' ^ c')) == ((a ^ c) v (b' ^ c')))
124wr4 199 . . . . 5 (a' == b') = 1
1312wran 369 . . . 4 ((a' ^ c') == (b' ^ c')) = 1
1413wlor 368 . . 3 (((a ^ c) v (a' ^ c')) == ((a ^ c) v (b' ^ c'))) = 1
1511, 14ax-r2 36 . 2 ((a == c) == ((a ^ c) v (b' ^ c'))) = 1
169, 15wwbmpr 206 1 (a == c) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8
This theorem is referenced by:  w2or  372  w2an  373  w3tr1  374  wleoa  376  wleao  377  wom5  381  wcomlem  382  wdf-c1  383  wlea  388  wlel  392  wleror  393  wleran  394  wletr  396  wbltr  397  wlbtr  398  wbile  401  wlebi  402  wlecom  409  wcbtr  411  wcomcom2  415  wcomd  418  wcom3ii  419  wcomdr  421  wcom3i  422  wfh1  423  wfh2  424  wfh3  425  wfh4  426  wcom2or  427  wnbdi  429  ska2  432  woml6  436  woml7  437  wddi2  1106  wddi4  1108  wdid0id5  1109  wdid0id1  1110  wdid0id2  1111  wdid0id3  1112  wdid0id4  1113
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-wom 361
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le1 130  df-le2 131
  Copyright terms: Public domain W3C validator