QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  u4lem5 Unicode version
Theorem u4lem5 764
Description: Lemma for unified implication study.
Assertion
Ref Expression
u4lem5 (a ->4 (a ->4 b)) = ((a' ^ b') v b)
Proof of Theorem u4lem5
StepHypRef Expression
1 df-i4 47 . 2 (a ->4 (a ->4 b)) = (((a ^ (a ->4 b)) v (a' ^ (a ->4 b))) v ((a' v (a ->4 b)) ^ (a ->4 b)'))
2 ancom 74 . . . . . . 7 (a ^ (a ->4 b)) = ((a ->4 b) ^ a)
3 u4lemaa 603 . . . . . . 7 ((a ->4 b) ^ a) = (a ^ b)
42, 3ax-r2 36 . . . . . 6 (a ^ (a ->4 b)) = (a ^ b)
5 ancom 74 . . . . . . 7 (a' ^ (a ->4 b)) = ((a ->4 b) ^ a')
6 u4lemana 608 . . . . . . 7 ((a ->4 b) ^ a') = ((a' ^ b) v (a' ^ b'))
75, 6ax-r2 36 . . . . . 6 (a' ^ (a ->4 b)) = ((a' ^ b) v (a' ^ b'))
84, 72or 72 . . . . 5 ((a ^ (a ->4 b)) v (a' ^ (a ->4 b))) = ((a ^ b) v ((a' ^ b) v (a' ^ b')))
9 ax-a3 32 . . . . . 6 (((a ^ b) v (a' ^ b)) v (a' ^ b')) = ((a ^ b) v ((a' ^ b) v (a' ^ b')))
109ax-r1 35 . . . . 5 ((a ^ b) v ((a' ^ b) v (a' ^ b'))) = (((a ^ b) v (a' ^ b)) v (a' ^ b'))
118, 10ax-r2 36 . . . 4 ((a ^ (a ->4 b)) v (a' ^ (a ->4 b))) = (((a ^ b) v (a' ^ b)) v (a' ^ b'))
12 ax-a2 31 . . . . . . 7 (a' v (a ->4 b)) = ((a ->4 b) v a')
13 u4lemona 628 . . . . . . 7 ((a ->4 b) v a') = (a' v b)
1412, 13ax-r2 36 . . . . . 6 (a' v (a ->4 b)) = (a' v b)
15 ud4lem0c 280 . . . . . 6 (a ->4 b)' = (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))
1614, 152an 79 . . . . 5 ((a' v (a ->4 b)) ^ (a ->4 b)') = ((a' v b) ^ (((a' v b') ^ (a v b')) ^ ((a ^ b') v b)))
17 ancom 74 . . . . . 6 ((a' v b) ^ (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))) = ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (a' v b))
18 anass 76 . . . . . . 7 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (a' v b)) = (((a' v b') ^ (a v b')) ^ (((a ^ b') v b) ^ (a' v b)))
19 comor1 461 . . . . . . . . . . . . 13 (a' v b) C a'
2019comcom7 460 . . . . . . . . . . . 12 (a' v b) C a
21 comor2 462 . . . . . . . . . . . . 13 (a' v b) C b
2221comcom2 183 . . . . . . . . . . . 12 (a' v b) C b'
2320, 22com2an 484 . . . . . . . . . . 11 (a' v b) C (a ^ b')
2423, 21fh1r 473 . . . . . . . . . 10 (((a ^ b') v b) ^ (a' v b)) = (((a ^ b') ^ (a' v b)) v (b ^ (a' v b)))
25 ax-a2 31 . . . . . . . . . . 11 (((a ^ b') ^ (a' v b)) v (b ^ (a' v b))) = ((b ^ (a' v b)) v ((a ^ b') ^ (a' v b)))
26 leor 159 . . . . . . . . . . . . . 14 b =< (a' v b)
2726df2le2 136 . . . . . . . . . . . . 13 (b ^ (a' v b)) = b
28 oran2 92 . . . . . . . . . . . . . . 15 (a' v b) = (a ^ b')'
2928lan 77 . . . . . . . . . . . . . 14 ((a ^ b') ^ (a' v b)) = ((a ^ b') ^ (a ^ b')')
30 dff 101 . . . . . . . . . . . . . . 15 0 = ((a ^ b') ^ (a ^ b')')
3130ax-r1 35 . . . . . . . . . . . . . 14 ((a ^ b') ^ (a ^ b')') = 0
3229, 31ax-r2 36 . . . . . . . . . . . . 13 ((a ^ b') ^ (a' v b)) = 0
3327, 322or 72 . . . . . . . . . . . 12 ((b ^ (a' v b)) v ((a ^ b') ^ (a' v b))) = (b v 0)
34 or0 102 . . . . . . . . . . . 12 (b v 0) = b
3533, 34ax-r2 36 . . . . . . . . . . 11 ((b ^ (a' v b)) v ((a ^ b') ^ (a' v b))) = b
3625, 35ax-r2 36 . . . . . . . . . 10 (((a ^ b') ^ (a' v b)) v (b ^ (a' v b))) = b
3724, 36ax-r2 36 . . . . . . . . 9 (((a ^ b') v b) ^ (a' v b)) = b
3837lan 77 . . . . . . . 8 (((a' v b') ^ (a v b')) ^ (((a ^ b') v b) ^ (a' v b))) = (((a' v b') ^ (a v b')) ^ b)
39 ancom 74 . . . . . . . 8 (((a' v b') ^ (a v b')) ^ b) = (b ^ ((a' v b') ^ (a v b')))
4038, 39ax-r2 36 . . . . . . 7 (((a' v b') ^ (a v b')) ^ (((a ^ b') v b) ^ (a' v b))) = (b ^ ((a' v b') ^ (a v b')))
4118, 40ax-r2 36 . . . . . 6 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (a' v b)) = (b ^ ((a' v b') ^ (a v b')))
4217, 41ax-r2 36 . . . . 5 ((a' v b) ^ (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))) = (b ^ ((a' v b') ^ (a v b')))
4316, 42ax-r2 36 . . . 4 ((a' v (a ->4 b)) ^ (a ->4 b)') = (b ^ ((a' v b') ^ (a v b')))
4411, 432or 72 . . 3 (((a ^ (a ->4 b)) v (a' ^ (a ->4 b))) v ((a' v (a ->4 b)) ^ (a ->4 b)')) = ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (b ^ ((a' v b') ^ (a v b'))))
45 comanr2 465 . . . . . . 7 b C (a ^ b)
46 comanr2 465 . . . . . . 7 b C (a' ^ b)
4745, 46com2or 483 . . . . . 6 b C ((a ^ b) v (a' ^ b))
48 comanr2 465 . . . . . . 7 b' C (a' ^ b')
4948comcom6 459 . . . . . 6 b C (a' ^ b')
5047, 49com2or 483 . . . . 5 b C (((a ^ b) v (a' ^ b)) v (a' ^ b'))
51 comorr2 463 . . . . . . 7 b' C (a' v b')
52 comorr2 463 . . . . . . 7 b' C (a v b')
5351, 52com2an 484 . . . . . 6 b' C ((a' v b') ^ (a v b'))
5453comcom6 459 . . . . 5 b C ((a' v b') ^ (a v b'))
5550, 54fh4 472 . . . 4 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (b ^ ((a' v b') ^ (a v b')))) = (((((a ^ b) v (a' ^ b)) v (a' ^ b')) v b) ^ ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v ((a' v b') ^ (a v b'))))
56 or32 82 . . . . . . 7 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v b) = ((((a ^ b) v (a' ^ b)) v b) v (a' ^ b'))
57 lear 161 . . . . . . . . . 10 (a ^ b) =< b
58 lear 161 . . . . . . . . . 10 (a' ^ b) =< b
5957, 58lel2or 170 . . . . . . . . 9 ((a ^ b) v (a' ^ b)) =< b
6059df-le2 131 . . . . . . . 8 (((a ^ b) v (a' ^ b)) v b) = b
6160ax-r5 38 . . . . . . 7 ((((a ^ b) v (a' ^ b)) v b) v (a' ^ b')) = (b v (a' ^ b'))
6256, 61ax-r2 36 . . . . . 6 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v b) = (b v (a' ^ b'))
63 comor1 461 . . . . . . . . . . . 12 (a' v b') C a'
6463comcom7 460 . . . . . . . . . . 11 (a' v b') C a
65 comor2 462 . . . . . . . . . . . 12 (a' v b') C b'
6665comcom7 460 . . . . . . . . . . 11 (a' v b') C b
6764, 66com2an 484 . . . . . . . . . 10 (a' v b') C (a ^ b)
6863, 66com2an 484 . . . . . . . . . 10 (a' v b') C (a' ^ b)
6967, 68com2or 483 . . . . . . . . 9 (a' v b') C ((a ^ b) v (a' ^ b))
7063, 65com2an 484 . . . . . . . . 9 (a' v b') C (a' ^ b')
7169, 70com2or 483 . . . . . . . 8 (a' v b') C (((a ^ b) v (a' ^ b)) v (a' ^ b'))
7264, 65com2or 483 . . . . . . . 8 (a' v b') C (a v b')
7371, 72fh4 472 . . . . . . 7 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v ((a' v b') ^ (a v b'))) = (((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (a' v b')) ^ ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (a v b')))
74 or32 82 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (a' v b')) = ((((a ^ b) v (a' ^ b)) v (a' v b')) v (a' ^ b'))
75 ax-a3 32 . . . . . . . . . . 11 ((((a ^ b) v (a' ^ b)) v (a' v b')) v (a' ^ b')) = (((a ^ b) v (a' ^ b)) v ((a' v b') v (a' ^ b')))
76 or4 84 . . . . . . . . . . . 12 (((a ^ b) v (a' ^ b)) v ((a' v b') v (a' ^ b'))) = (((a ^ b) v (a' v b')) v ((a' ^ b) v (a' ^ b')))
77 ax-a2 31 . . . . . . . . . . . . 13 (((a ^ b) v (a' v b')) v ((a' ^ b) v (a' ^ b'))) = (((a' ^ b) v (a' ^ b')) v ((a ^ b) v (a' v b')))
78 oran3 93 . . . . . . . . . . . . . . . . 17 (a' v b') = (a ^ b)'
7978lor 70 . . . . . . . . . . . . . . . 16 ((a ^ b) v (a' v b')) = ((a ^ b) v (a ^ b)')
80 df-t 41 . . . . . . . . . . . . . . . . 17 1 = ((a ^ b) v (a ^ b)')
8180ax-r1 35 . . . . . . . . . . . . . . . 16 ((a ^ b) v (a ^ b)') = 1
8279, 81ax-r2 36 . . . . . . . . . . . . . . 15 ((a ^ b) v (a' v b')) = 1
8382lor 70 . . . . . . . . . . . . . 14 (((a' ^ b) v (a' ^ b')) v ((a ^ b) v (a' v b'))) = (((a' ^ b) v (a' ^ b')) v 1)
84 or1 104 . . . . . . . . . . . . . 14 (((a' ^ b) v (a' ^ b')) v 1) = 1
8583, 84ax-r2 36 . . . . . . . . . . . . 13 (((a' ^ b) v (a' ^ b')) v ((a ^ b) v (a' v b'))) = 1
8677, 85ax-r2 36 . . . . . . . . . . . 12 (((a ^ b) v (a' v b')) v ((a' ^ b) v (a' ^ b'))) = 1
8776, 86ax-r2 36 . . . . . . . . . . 11 (((a ^ b) v (a' ^ b)) v ((a' v b') v (a' ^ b'))) = 1
8875, 87ax-r2 36 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b)) v (a' v b')) v (a' ^ b')) = 1
8974, 88ax-r2 36 . . . . . . . . 9 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (a' v b')) = 1
90 ax-a3 32 . . . . . . . . . 10 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (a v b')) = (((a ^ b) v (a' ^ b)) v ((a' ^ b') v (a v b')))
91 or4 84 . . . . . . . . . . 11 (((a ^ b) v (a' ^ b)) v ((a' ^ b') v (a v b'))) = (((a ^ b) v (a' ^ b')) v ((a' ^ b) v (a v b')))
92 oran1 91 . . . . . . . . . . . . . . 15 (a v b') = (a' ^ b)'
9392lor 70 . . . . . . . . . . . . . 14 ((a' ^ b) v (a v b')) = ((a' ^ b) v (a' ^ b)')
94 df-t 41 . . . . . . . . . . . . . . 15 1 = ((a' ^ b) v (a' ^ b)')
9594ax-r1 35 . . . . . . . . . . . . . 14 ((a' ^ b) v (a' ^ b)') = 1
9693, 95ax-r2 36 . . . . . . . . . . . . 13 ((a' ^ b) v (a v b')) = 1
9796lor 70 . . . . . . . . . . . 12 (((a ^ b) v (a' ^ b')) v ((a' ^ b) v (a v b'))) = (((a ^ b) v (a' ^ b')) v 1)
98 or1 104 . . . . . . . . . . . 12 (((a ^ b) v (a' ^ b')) v 1) = 1
9997, 98ax-r2 36 . . . . . . . . . . 11 (((a ^ b) v (a' ^ b')) v ((a' ^ b) v (a v b'))) = 1
10091, 99ax-r2 36 . . . . . . . . . 10 (((a ^ b) v (a' ^ b)) v ((a' ^ b') v (a v b'))) = 1
10190, 100ax-r2 36 . . . . . . . . 9 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (a v b')) = 1
10289, 1012an 79 . . . . . . . 8 (((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (a' v b')) ^ ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (a v b'))) = (1 ^ 1)
103 an1 106 . . . . . . . 8 (1 ^ 1) = 1
104102, 103ax-r2 36 . . . . . . 7 (((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (a' v b')) ^ ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (a v b'))) = 1
10573, 104ax-r2 36 . . . . . 6 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v ((a' v b') ^ (a v b'))) = 1
10662, 1052an 79 . . . . 5 (((((a ^ b) v (a' ^ b)) v (a' ^ b')) v b) ^ ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v ((a' v b') ^ (a v b')))) = ((b v (a' ^ b')) ^ 1)
107 an1 106 . . . . . 6 ((b v (a' ^ b')) ^ 1) = (b v (a' ^ b'))
108 ax-a2 31 . . . . . 6 (b v (a' ^ b')) = ((a' ^ b') v b)
109107, 108ax-r2 36 . . . . 5 ((b v (a' ^ b')) ^ 1) = ((a' ^ b') v b)
110106, 109ax-r2 36 . . . 4 (((((a ^ b) v (a' ^ b)) v (a' ^ b')) v b) ^ ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v ((a' v b') ^ (a v b')))) = ((a' ^ b') v b)
11155, 110ax-r2 36 . . 3 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (b ^ ((a' v b') ^ (a v b')))) = ((a' ^ b') v b)
11244, 111ax-r2 36 . 2 (((a ^ (a ->4 b)) v (a' ^ (a ->4 b))) v ((a' v (a ->4 b)) ^ (a ->4 b)')) = ((a' ^ b') v b)
1131, 112ax-r2 36 1 (a ->4 (a ->4 b)) = ((a' ^ b') v b)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8  0wf 9   ->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:  u4lem5n  766  u4lem6  768
  Copyright terms: Public domain W3C validator