QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  lem3.3.4 Unicode version
Theorem lem3.3.4 1053
Description: Equation 3.4 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
Hypothesis
Ref Expression
lem3.3.4.1 (b ->2 a) = 1
Assertion
Ref Expression
lem3.3.4 (a ->2 (a ==5 b)) = (a ==5 b)
Proof of Theorem lem3.3.4
StepHypRef Expression
1 df-i2 45 . 2 (a ->2 (a ==5 b)) = ((a ==5 b) v (a' ^ (a ==5 b)'))
2 df-id5 1047 . . . . . . 7 (a ==5 b) = ((a ^ b) v (a' ^ b'))
32ax-r4 37 . . . . . 6 (a ==5 b)' = ((a ^ b) v (a' ^ b'))'
43lan 77 . . . . 5 (a' ^ (a ==5 b)') = (a' ^ ((a ^ b) v (a' ^ b'))')
5 anor3 90 . . . . . . . 8 ((a ^ b)' ^ (a' ^ b')') = ((a ^ b) v (a' ^ b'))'
65ax-r1 35 . . . . . . 7 ((a ^ b) v (a' ^ b'))' = ((a ^ b)' ^ (a' ^ b')')
7 oran3 93 . . . . . . . . 9 (a' v b') = (a ^ b)'
87ax-r1 35 . . . . . . . 8 (a ^ b)' = (a' v b')
9 oran 87 . . . . . . . . 9 (a v b) = (a' ^ b')'
109ax-r1 35 . . . . . . . 8 (a' ^ b')' = (a v b)
118, 102an 79 . . . . . . 7 ((a ^ b)' ^ (a' ^ b')') = ((a' v b') ^ (a v b))
126, 11ax-r2 36 . . . . . 6 ((a ^ b) v (a' ^ b'))' = ((a' v b') ^ (a v b))
1312lan 77 . . . . 5 (a' ^ ((a ^ b) v (a' ^ b'))') = (a' ^ ((a' v b') ^ (a v b)))
14 anabs 121 . . . . . . 7 (a' ^ (a' v b')) = a'
1514ran 78 . . . . . 6 ((a' ^ (a' v b')) ^ (a v b)) = (a' ^ (a v b))
16 anass 76 . . . . . 6 ((a' ^ (a' v b')) ^ (a v b)) = (a' ^ ((a' v b') ^ (a v b)))
17 lem3.3.4.1 . . . . . . . 8 (b ->2 a) = 1
1817ax-r4 37 . . . . . . 7 (b ->2 a)' = 1'
199con2 67 . . . . . . . . . . 11 (a v b)' = (a' ^ b')
20 ancom 74 . . . . . . . . . . 11 (a' ^ b') = (b' ^ a')
2119, 20ax-r2 36 . . . . . . . . . 10 (a v b)' = (b' ^ a')
2221lor 70 . . . . . . . . 9 (a v (a v b)') = (a v (b' ^ a'))
23 oran1 91 . . . . . . . . . 10 (a v (a v b)') = (a' ^ (a v b))'
2423ax-r1 35 . . . . . . . . 9 (a' ^ (a v b))' = (a v (a v b)')
25 df-i2 45 . . . . . . . . 9 (b ->2 a) = (a v (b' ^ a'))
2622, 24, 253tr1 63 . . . . . . . 8 (a' ^ (a v b))' = (b ->2 a)
2726con3 68 . . . . . . 7 (a' ^ (a v b)) = (b ->2 a)'
28 df-f 42 . . . . . . 7 0 = 1'
2918, 27, 283tr1 63 . . . . . 6 (a' ^ (a v b)) = 0
3015, 16, 293tr2 64 . . . . 5 (a' ^ ((a' v b') ^ (a v b))) = 0
314, 13, 303tr 65 . . . 4 (a' ^ (a ==5 b)') = 0
3231lor 70 . . 3 ((a ==5 b) v (a' ^ (a ==5 b)')) = ((a ==5 b) v 0)
33 ax-a2 31 . . 3 ((a ==5 b) v 0) = (0 v (a ==5 b))
3432, 33ax-r2 36 . 2 ((a ==5 b) v (a' ^ (a ==5 b)')) = (0 v (a ==5 b))
35 or0r 103 . 2 (0 v (a ==5 b)) = (a ==5 b)
361, 34, 353tr 65 1 (a ->2 (a ==5 b)) = (a ==5 b)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8  0wf 9   ->2 wi2 13   ==5 wid5 22
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-i2 45  df-id5 1047
This theorem is referenced by:  lem3.4.4  1077
  Copyright terms: Public domain W3C validator