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

Theorem 3vth9 812
Description: A 3-variable theorem. (Contributed by NM, 16-Nov-1998.)
Assertion
Ref Expression
3vth9 ((ab) →1 (c2 b)) = ((bc) →2 (a2 b))

Proof of Theorem 3vth9
StepHypRef Expression
1 anor3 90 . . . 4 (ab ) = (ab)
21ax-r1 35 . . 3 (ab) = (ab )
3 df-i2 45 . . . 4 (c2 b) = (b ∪ (cb ))
43lan 77 . . 3 ((ab) ∩ (c2 b)) = ((ab) ∩ (b ∪ (cb )))
52, 42or 72 . 2 ((ab) ∪ ((ab) ∩ (c2 b))) = ((ab ) ∪ ((ab) ∩ (b ∪ (cb ))))
6 df-i1 44 . 2 ((ab) →1 (c2 b)) = ((ab) ∪ ((ab) ∩ (c2 b)))
7 df-i2 45 . . . 4 ((bc) →2 (a2 b)) = ((a2 b) ∪ ((bc) ∩ (a2 b) ))
8 df-i2 45 . . . . 5 (a2 b) = (b ∪ (ab ))
9 anor3 90 . . . . . . . 8 (bc ) = (bc)
109ax-r1 35 . . . . . . 7 (bc) = (bc )
11 ud2lem0c 278 . . . . . . 7 (a2 b) = (b ∩ (ab))
1210, 112an 79 . . . . . 6 ((bc) ∩ (a2 b) ) = ((bc ) ∩ (b ∩ (ab)))
13 anandi 114 . . . . . . . 8 (b ∩ (c ∩ (ab))) = ((bc ) ∩ (b ∩ (ab)))
1413ax-r1 35 . . . . . . 7 ((bc ) ∩ (b ∩ (ab))) = (b ∩ (c ∩ (ab)))
15 anass 76 . . . . . . . 8 ((bc ) ∩ (ab)) = (b ∩ (c ∩ (ab)))
1615ax-r1 35 . . . . . . 7 (b ∩ (c ∩ (ab))) = ((bc ) ∩ (ab))
1714, 16ax-r2 36 . . . . . 6 ((bc ) ∩ (b ∩ (ab))) = ((bc ) ∩ (ab))
1812, 17ax-r2 36 . . . . 5 ((bc) ∩ (a2 b) ) = ((bc ) ∩ (ab))
198, 182or 72 . . . 4 ((a2 b) ∪ ((bc) ∩ (a2 b) )) = ((b ∪ (ab )) ∪ ((bc ) ∩ (ab)))
207, 19ax-r2 36 . . 3 ((bc) →2 (a2 b)) = ((b ∪ (ab )) ∪ ((bc ) ∩ (ab)))
21 or32 82 . . . 4 ((b ∪ (ab )) ∪ ((bc ) ∩ (ab))) = ((b ∪ ((bc ) ∩ (ab))) ∪ (ab ))
22 comanr1 464 . . . . . . . . 9 b C (bc )
2322comcom6 459 . . . . . . . 8 b C (bc )
24 comorr2 463 . . . . . . . 8 b C (ab)
2523, 24fh3 471 . . . . . . 7 (b ∪ ((bc ) ∩ (ab))) = ((b ∪ (bc )) ∩ (b ∪ (ab)))
26 ancom 74 . . . . . . . . . 10 (bc ) = (cb )
2726lor 70 . . . . . . . . 9 (b ∪ (bc )) = (b ∪ (cb ))
28 or12 80 . . . . . . . . . 10 (b ∪ (ab)) = (a ∪ (bb))
29 oridm 110 . . . . . . . . . . 11 (bb) = b
3029lor 70 . . . . . . . . . 10 (a ∪ (bb)) = (ab)
3128, 30ax-r2 36 . . . . . . . . 9 (b ∪ (ab)) = (ab)
3227, 312an 79 . . . . . . . 8 ((b ∪ (bc )) ∩ (b ∪ (ab))) = ((b ∪ (cb )) ∩ (ab))
33 ancom 74 . . . . . . . 8 ((b ∪ (cb )) ∩ (ab)) = ((ab) ∩ (b ∪ (cb )))
3432, 33ax-r2 36 . . . . . . 7 ((b ∪ (bc )) ∩ (b ∪ (ab))) = ((ab) ∩ (b ∪ (cb )))
3525, 34ax-r2 36 . . . . . 6 (b ∪ ((bc ) ∩ (ab))) = ((ab) ∩ (b ∪ (cb )))
3635ax-r5 38 . . . . 5 ((b ∪ ((bc ) ∩ (ab))) ∪ (ab )) = (((ab) ∩ (b ∪ (cb ))) ∪ (ab ))
37 ax-a2 31 . . . . 5 (((ab) ∩ (b ∪ (cb ))) ∪ (ab )) = ((ab ) ∪ ((ab) ∩ (b ∪ (cb ))))
3836, 37ax-r2 36 . . . 4 ((b ∪ ((bc ) ∩ (ab))) ∪ (ab )) = ((ab ) ∪ ((ab) ∩ (b ∪ (cb ))))
3921, 38ax-r2 36 . . 3 ((b ∪ (ab )) ∪ ((bc ) ∩ (ab))) = ((ab ) ∪ ((ab) ∩ (b ∪ (cb ))))
4020, 39ax-r2 36 . 2 ((bc) →2 (a2 b)) = ((ab ) ∪ ((ab) ∩ (b ∪ (cb ))))
415, 6, 403tr1 63 1 ((ab) →1 (c2 b)) = ((bc) →2 (a2 b))
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  1 wi1 12  2 wi2 13
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-r3 439
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  df-c1 132  df-c2 133
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator