QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  u4lemona Unicode version
Theorem u4lemona 628
Description: Lemma for non-tollens implication study.
Assertion
Ref Expression
u4lemona ((a ->4 b) v a') = (a' v b)
Proof of Theorem u4lemona
StepHypRef Expression
1 df-i4 47 . . 3 (a ->4 b) = (((a ^ b) v (a' ^ b)) v ((a' v b) ^ b'))
21ax-r5 38 . 2 ((a ->4 b) v a') = ((((a ^ b) v (a' ^ b)) v ((a' v b) ^ b')) v a')
3 or32 82 . . 3 ((((a ^ b) v (a' ^ b)) v ((a' v b) ^ b')) v a') = ((((a ^ b) v (a' ^ b)) v a') v ((a' v b) ^ b'))
4 ax-a3 32 . . . . . 6 (((a ^ b) v (a' ^ b)) v a') = ((a ^ b) v ((a' ^ b) v a'))
5 lea 160 . . . . . . . 8 (a' ^ b) =< a'
65df-le2 131 . . . . . . 7 ((a' ^ b) v a') = a'
76lor 70 . . . . . 6 ((a ^ b) v ((a' ^ b) v a')) = ((a ^ b) v a')
84, 7ax-r2 36 . . . . 5 (((a ^ b) v (a' ^ b)) v a') = ((a ^ b) v a')
98ax-r5 38 . . . 4 ((((a ^ b) v (a' ^ b)) v a') v ((a' v b) ^ b')) = (((a ^ b) v a') v ((a' v b) ^ b'))
10 comor1 461 . . . . . . . . 9 (a' v b) C a'
1110comcom7 460 . . . . . . . 8 (a' v b) C a
12 comor2 462 . . . . . . . 8 (a' v b) C b
1311, 12com2an 484 . . . . . . 7 (a' v b) C (a ^ b)
1413, 10com2or 483 . . . . . 6 (a' v b) C ((a ^ b) v a')
1512comcom2 183 . . . . . 6 (a' v b) C b'
1614, 15fh4 472 . . . . 5 (((a ^ b) v a') v ((a' v b) ^ b')) = ((((a ^ b) v a') v (a' v b)) ^ (((a ^ b) v a') v b'))
17 lear 161 . . . . . . . . . 10 (a ^ b) =< b
18 leor 159 . . . . . . . . . 10 b =< (a' v b)
1917, 18letr 137 . . . . . . . . 9 (a ^ b) =< (a' v b)
20 leo 158 . . . . . . . . 9 a' =< (a' v b)
2119, 20lel2or 170 . . . . . . . 8 ((a ^ b) v a') =< (a' v b)
2221df-le2 131 . . . . . . 7 (((a ^ b) v a') v (a' v b)) = (a' v b)
23 ax-a3 32 . . . . . . . 8 (((a ^ b) v a') v b') = ((a ^ b) v (a' v b'))
24 df-a 40 . . . . . . . . . . . 12 (a ^ b) = (a' v b')'
2524ax-r1 35 . . . . . . . . . . 11 (a' v b')' = (a ^ b)
2625con3 68 . . . . . . . . . 10 (a' v b') = (a ^ b)'
2726lor 70 . . . . . . . . 9 ((a ^ b) v (a' v b')) = ((a ^ b) v (a ^ b)')
28 df-t 41 . . . . . . . . . 10 1 = ((a ^ b) v (a ^ b)')
2928ax-r1 35 . . . . . . . . 9 ((a ^ b) v (a ^ b)') = 1
3027, 29ax-r2 36 . . . . . . . 8 ((a ^ b) v (a' v b')) = 1
3123, 30ax-r2 36 . . . . . . 7 (((a ^ b) v a') v b') = 1
3222, 312an 79 . . . . . 6 ((((a ^ b) v a') v (a' v b)) ^ (((a ^ b) v a') v b')) = ((a' v b) ^ 1)
33 an1 106 . . . . . 6 ((a' v b) ^ 1) = (a' v b)
3432, 33ax-r2 36 . . . . 5 ((((a ^ b) v a') v (a' v b)) ^ (((a ^ b) v a') v b')) = (a' v b)
3516, 34ax-r2 36 . . . 4 (((a ^ b) v a') v ((a' v b) ^ b')) = (a' v b)
369, 35ax-r2 36 . . 3 ((((a ^ b) v (a' ^ b)) v a') v ((a' v b) ^ b')) = (a' v b)
373, 36ax-r2 36 . 2 ((((a ^ b) v (a' ^ b)) v ((a' v b) ^ b')) v a') = (a' v b)
382, 37ax-r2 36 1 ((a ->4 b) v a') = (a' v b)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8   ->4 wi4 15
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-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  u4lemnaa  643  u4lem5  764
  Copyright terms: Public domain W3C validator