QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  3vth9 Unicode version
Theorem 3vth9 812
Description: A 3-variable theorem.
Assertion
Ref Expression
3vth9 ((a v b) ->1 (c ->2 b)) = ((b v c) ->2 (a ->2 b))
Proof of Theorem 3vth9
StepHypRef Expression
1 anor3 90 . . . 4 (a' ^ b') = (a v b)'
21ax-r1 35 . . 3 (a v b)' = (a' ^ b')
3 df-i2 45 . . . 4 (c ->2 b) = (b v (c' ^ b'))
43lan 77 . . 3 ((a v b) ^ (c ->2 b)) = ((a v b) ^ (b v (c' ^ b')))
52, 42or 72 . 2 ((a v b)' v ((a v b) ^ (c ->2 b))) = ((a' ^ b') v ((a v b) ^ (b v (c' ^ b'))))
6 df-i1 44 . 2 ((a v b) ->1 (c ->2 b)) = ((a v b)' v ((a v b) ^ (c ->2 b)))
7 df-i2 45 . . . 4 ((b v c) ->2 (a ->2 b)) = ((a ->2 b) v ((b v c)' ^ (a ->2 b)'))
8 df-i2 45 . . . . 5 (a ->2 b) = (b v (a' ^ b'))
9 anor3 90 . . . . . . . 8 (b' ^ c') = (b v c)'
109ax-r1 35 . . . . . . 7 (b v c)' = (b' ^ c')
11 ud2lem0c 278 . . . . . . 7 (a ->2 b)' = (b' ^ (a v b))
1210, 112an 79 . . . . . 6 ((b v c)' ^ (a ->2 b)') = ((b' ^ c') ^ (b' ^ (a v b)))
13 anandi 114 . . . . . . . 8 (b' ^ (c' ^ (a v b))) = ((b' ^ c') ^ (b' ^ (a v b)))
1413ax-r1 35 . . . . . . 7 ((b' ^ c') ^ (b' ^ (a v b))) = (b' ^ (c' ^ (a v b)))
15 anass 76 . . . . . . . 8 ((b' ^ c') ^ (a v b)) = (b' ^ (c' ^ (a v b)))
1615ax-r1 35 . . . . . . 7 (b' ^ (c' ^ (a v b))) = ((b' ^ c') ^ (a v b))
1714, 16ax-r2 36 . . . . . 6 ((b' ^ c') ^ (b' ^ (a v b))) = ((b' ^ c') ^ (a v b))
1812, 17ax-r2 36 . . . . 5 ((b v c)' ^ (a ->2 b)') = ((b' ^ c') ^ (a v b))
198, 182or 72 . . . 4 ((a ->2 b) v ((b v c)' ^ (a ->2 b)')) = ((b v (a' ^ b')) v ((b' ^ c') ^ (a v b)))
207, 19ax-r2 36 . . 3 ((b v c) ->2 (a ->2 b)) = ((b v (a' ^ b')) v ((b' ^ c') ^ (a v b)))
21 or32 82 . . . 4 ((b v (a' ^ b')) v ((b' ^ c') ^ (a v b))) = ((b v ((b' ^ c') ^ (a v b))) v (a' ^ b'))
22 comanr1 464 . . . . . . . . 9 b' C (b' ^ c')
2322comcom6 459 . . . . . . . 8 b C (b' ^ c')
24 comorr2 463 . . . . . . . 8 b C (a v b)
2523, 24fh3 471 . . . . . . 7 (b v ((b' ^ c') ^ (a v b))) = ((b v (b' ^ c')) ^ (b v (a v b)))
26 ancom 74 . . . . . . . . . 10 (b' ^ c') = (c' ^ b')
2726lor 70 . . . . . . . . 9 (b v (b' ^ c')) = (b v (c' ^ b'))
28 or12 80 . . . . . . . . . 10 (b v (a v b)) = (a v (b v b))
29 oridm 110 . . . . . . . . . . 11 (b v b) = b
3029lor 70 . . . . . . . . . 10 (a v (b v b)) = (a v b)
3128, 30ax-r2 36 . . . . . . . . 9 (b v (a v b)) = (a v b)
3227, 312an 79 . . . . . . . 8 ((b v (b' ^ c')) ^ (b v (a v b))) = ((b v (c' ^ b')) ^ (a v b))
33 ancom 74 . . . . . . . 8 ((b v (c' ^ b')) ^ (a v b)) = ((a v b) ^ (b v (c' ^ b')))
3432, 33ax-r2 36 . . . . . . 7 ((b v (b' ^ c')) ^ (b v (a v b))) = ((a v b) ^ (b v (c' ^ b')))
3525, 34ax-r2 36 . . . . . 6 (b v ((b' ^ c') ^ (a v b))) = ((a v b) ^ (b v (c' ^ b')))
3635ax-r5 38 . . . . 5 ((b v ((b' ^ c') ^ (a v b))) v (a' ^ b')) = (((a v b) ^ (b v (c' ^ b'))) v (a' ^ b'))
37 ax-a2 31 . . . . 5 (((a v b) ^ (b v (c' ^ b'))) v (a' ^ b')) = ((a' ^ b') v ((a v b) ^ (b v (c' ^ b'))))
3836, 37ax-r2 36 . . . 4 ((b v ((b' ^ c') ^ (a v b))) v (a' ^ b')) = ((a' ^ b') v ((a v b) ^ (b v (c' ^ b'))))
3921, 38ax-r2 36 . . 3 ((b v (a' ^ b')) v ((b' ^ c') ^ (a v b))) = ((a' ^ b') v ((a v b) ^ (b v (c' ^ b'))))
4020, 39ax-r2 36 . 2 ((b v c) ->2 (a ->2 b)) = ((a' ^ b') v ((a v b) ^ (b v (c' ^ b'))))
415, 6, 403tr1 63 1 ((a v b) ->1 (c ->2 b)) = ((b v c) ->2 (a ->2 b))
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v 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