QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  u4lem6 Unicode version
Theorem u4lem6 768
Description: Lemma for unified implication study.
Assertion
Ref Expression
u4lem6 (a ->4 (a ->4 (a ->4 b))) = (a ->4 b)
Proof of Theorem u4lem6
StepHypRef Expression
1 df-i4 47 . 2 (a ->4 (a ->4 (a ->4 b))) = (((a ^ (a ->4 (a ->4 b))) v (a' ^ (a ->4 (a ->4 b)))) v ((a' v (a ->4 (a ->4 b))) ^ (a ->4 (a ->4 b))'))
2 u4lem5 764 . . . . . . . 8 (a ->4 (a ->4 b)) = ((a' ^ b') v b)
32lan 77 . . . . . . 7 (a ^ (a ->4 (a ->4 b))) = (a ^ ((a' ^ b') v b))
4 coman1 185 . . . . . . . . . 10 (a' ^ b') C a'
54comcom7 460 . . . . . . . . 9 (a' ^ b') C a
6 coman2 186 . . . . . . . . . 10 (a' ^ b') C b'
76comcom7 460 . . . . . . . . 9 (a' ^ b') C b
85, 7fh2 470 . . . . . . . 8 (a ^ ((a' ^ b') v b)) = ((a ^ (a' ^ b')) v (a ^ b))
9 ax-a2 31 . . . . . . . . 9 ((a ^ (a' ^ b')) v (a ^ b)) = ((a ^ b) v (a ^ (a' ^ b')))
10 ancom 74 . . . . . . . . . . . 12 ((a ^ a') ^ b') = (b' ^ (a ^ a'))
11 anass 76 . . . . . . . . . . . 12 ((a ^ a') ^ b') = (a ^ (a' ^ b'))
12 dff 101 . . . . . . . . . . . . . . 15 0 = (a ^ a')
1312ax-r1 35 . . . . . . . . . . . . . 14 (a ^ a') = 0
1413lan 77 . . . . . . . . . . . . 13 (b' ^ (a ^ a')) = (b' ^ 0)
15 an0 108 . . . . . . . . . . . . 13 (b' ^ 0) = 0
1614, 15ax-r2 36 . . . . . . . . . . . 12 (b' ^ (a ^ a')) = 0
1710, 11, 163tr2 64 . . . . . . . . . . 11 (a ^ (a' ^ b')) = 0
1817lor 70 . . . . . . . . . 10 ((a ^ b) v (a ^ (a' ^ b'))) = ((a ^ b) v 0)
19 or0 102 . . . . . . . . . 10 ((a ^ b) v 0) = (a ^ b)
2018, 19ax-r2 36 . . . . . . . . 9 ((a ^ b) v (a ^ (a' ^ b'))) = (a ^ b)
219, 20ax-r2 36 . . . . . . . 8 ((a ^ (a' ^ b')) v (a ^ b)) = (a ^ b)
228, 21ax-r2 36 . . . . . . 7 (a ^ ((a' ^ b') v b)) = (a ^ b)
233, 22ax-r2 36 . . . . . 6 (a ^ (a ->4 (a ->4 b))) = (a ^ b)
242lan 77 . . . . . . 7 (a' ^ (a ->4 (a ->4 b))) = (a' ^ ((a' ^ b') v b))
254, 7fh2 470 . . . . . . . 8 (a' ^ ((a' ^ b') v b)) = ((a' ^ (a' ^ b')) v (a' ^ b))
26 anass 76 . . . . . . . . . . 11 ((a' ^ a') ^ b') = (a' ^ (a' ^ b'))
2726ax-r1 35 . . . . . . . . . 10 (a' ^ (a' ^ b')) = ((a' ^ a') ^ b')
28 anidm 111 . . . . . . . . . . 11 (a' ^ a') = a'
2928ran 78 . . . . . . . . . 10 ((a' ^ a') ^ b') = (a' ^ b')
3027, 29ax-r2 36 . . . . . . . . 9 (a' ^ (a' ^ b')) = (a' ^ b')
3130ax-r5 38 . . . . . . . 8 ((a' ^ (a' ^ b')) v (a' ^ b)) = ((a' ^ b') v (a' ^ b))
3225, 31ax-r2 36 . . . . . . 7 (a' ^ ((a' ^ b') v b)) = ((a' ^ b') v (a' ^ b))
3324, 32ax-r2 36 . . . . . 6 (a' ^ (a ->4 (a ->4 b))) = ((a' ^ b') v (a' ^ b))
3423, 332or 72 . . . . 5 ((a ^ (a ->4 (a ->4 b))) v (a' ^ (a ->4 (a ->4 b)))) = ((a ^ b) v ((a' ^ b') v (a' ^ b)))
35 id 59 . . . . 5 ((a ^ b) v ((a' ^ b') v (a' ^ b))) = ((a ^ b) v ((a' ^ b') v (a' ^ b)))
3634, 35ax-r2 36 . . . 4 ((a ^ (a ->4 (a ->4 b))) v (a' ^ (a ->4 (a ->4 b)))) = ((a ^ b) v ((a' ^ b') v (a' ^ b)))
372lor 70 . . . . . . 7 (a' v (a ->4 (a ->4 b))) = (a' v ((a' ^ b') v b))
38 or12 80 . . . . . . . 8 (a' v ((a' ^ b') v b)) = ((a' ^ b') v (a' v b))
39 comor1 461 . . . . . . . . . 10 (a' v b) C a'
40 comor2 462 . . . . . . . . . . 11 (a' v b) C b
4140comcom2 183 . . . . . . . . . 10 (a' v b) C b'
4239, 41fh3r 475 . . . . . . . . 9 ((a' ^ b') v (a' v b)) = ((a' v (a' v b)) ^ (b' v (a' v b)))
43 ax-a3 32 . . . . . . . . . . . . 13 ((a' v a') v b) = (a' v (a' v b))
4443ax-r1 35 . . . . . . . . . . . 12 (a' v (a' v b)) = ((a' v a') v b)
45 oridm 110 . . . . . . . . . . . . 13 (a' v a') = a'
4645ax-r5 38 . . . . . . . . . . . 12 ((a' v a') v b) = (a' v b)
4744, 46ax-r2 36 . . . . . . . . . . 11 (a' v (a' v b)) = (a' v b)
48 or12 80 . . . . . . . . . . . 12 (b' v (a' v b)) = (a' v (b' v b))
49 ax-a2 31 . . . . . . . . . . . . . . 15 (b' v b) = (b v b')
50 df-t 41 . . . . . . . . . . . . . . . 16 1 = (b v b')
5150ax-r1 35 . . . . . . . . . . . . . . 15 (b v b') = 1
5249, 51ax-r2 36 . . . . . . . . . . . . . 14 (b' v b) = 1
5352lor 70 . . . . . . . . . . . . 13 (a' v (b' v b)) = (a' v 1)
54 or1 104 . . . . . . . . . . . . 13 (a' v 1) = 1
5553, 54ax-r2 36 . . . . . . . . . . . 12 (a' v (b' v b)) = 1
5648, 55ax-r2 36 . . . . . . . . . . 11 (b' v (a' v b)) = 1
5747, 562an 79 . . . . . . . . . 10 ((a' v (a' v b)) ^ (b' v (a' v b))) = ((a' v b) ^ 1)
58 an1 106 . . . . . . . . . 10 ((a' v b) ^ 1) = (a' v b)
5957, 58ax-r2 36 . . . . . . . . 9 ((a' v (a' v b)) ^ (b' v (a' v b))) = (a' v b)
6042, 59ax-r2 36 . . . . . . . 8 ((a' ^ b') v (a' v b)) = (a' v b)
6138, 60ax-r2 36 . . . . . . 7 (a' v ((a' ^ b') v b)) = (a' v b)
6237, 61ax-r2 36 . . . . . 6 (a' v (a ->4 (a ->4 b))) = (a' v b)
63 u4lem5n 766 . . . . . 6 (a ->4 (a ->4 b))' = ((a v b) ^ b')
6462, 632an 79 . . . . 5 ((a' v (a ->4 (a ->4 b))) ^ (a ->4 (a ->4 b))') = ((a' v b) ^ ((a v b) ^ b'))
65 id 59 . . . . 5 ((a' v b) ^ ((a v b) ^ b')) = ((a' v b) ^ ((a v b) ^ b'))
6664, 65ax-r2 36 . . . 4 ((a' v (a ->4 (a ->4 b))) ^ (a ->4 (a ->4 b))') = ((a' v b) ^ ((a v b) ^ b'))
6736, 662or 72 . . 3 (((a ^ (a ->4 (a ->4 b))) v (a' ^ (a ->4 (a ->4 b)))) v ((a' v (a ->4 (a ->4 b))) ^ (a ->4 (a ->4 b))')) = (((a ^ b) v ((a' ^ b') v (a' ^ b))) v ((a' v b) ^ ((a v b) ^ b')))
6839comcom7 460 . . . . . . 7 (a' v b) C a
6968, 40com2an 484 . . . . . 6 (a' v b) C (a ^ b)
7039, 41com2an 484 . . . . . . 7 (a' v b) C (a' ^ b')
7139, 40com2an 484 . . . . . . 7 (a' v b) C (a' ^ b)
7270, 71com2or 483 . . . . . 6 (a' v b) C ((a' ^ b') v (a' ^ b))
7369, 72com2or 483 . . . . 5 (a' v b) C ((a ^ b) v ((a' ^ b') v (a' ^ b)))
7468, 40com2or 483 . . . . . 6 (a' v b) C (a v b)
7574, 41com2an 484 . . . . 5 (a' v b) C ((a v b) ^ b')
7673, 75fh4 472 . . . 4 (((a ^ b) v ((a' ^ b') v (a' ^ b))) v ((a' v b) ^ ((a v b) ^ 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) ^ b')))
77 lear 161 . . . . . . . . 9 (a ^ b) =< b
78 leor 159 . . . . . . . . 9 b =< (a' v b)
7977, 78letr 137 . . . . . . . 8 (a ^ b) =< (a' v b)
80 lea 160 . . . . . . . . . 10 (a' ^ b') =< a'
81 lea 160 . . . . . . . . . 10 (a' ^ b) =< a'
8280, 81lel2or 170 . . . . . . . . 9 ((a' ^ b') v (a' ^ b)) =< a'
83 leo 158 . . . . . . . . 9 a' =< (a' v b)
8482, 83letr 137 . . . . . . . 8 ((a' ^ b') v (a' ^ b)) =< (a' v b)
8579, 84lel2or 170 . . . . . . 7 ((a ^ b) v ((a' ^ b') v (a' ^ b))) =< (a' v b)
8685df-le2 131 . . . . . 6 (((a ^ b) v ((a' ^ b') v (a' ^ b))) v (a' v b)) = (a' v b)
87 comor1 461 . . . . . . . . . 10 (a v b) C a
88 comor2 462 . . . . . . . . . 10 (a v b) C b
8987, 88com2an 484 . . . . . . . . 9 (a v b) C (a ^ b)
9087comcom2 183 . . . . . . . . . . 11 (a v b) C a'
9188comcom2 183 . . . . . . . . . . 11 (a v b) C b'
9290, 91com2an 484 . . . . . . . . . 10 (a v b) C (a' ^ b')
9390, 88com2an 484 . . . . . . . . . 10 (a v b) C (a' ^ b)
9492, 93com2or 483 . . . . . . . . 9 (a v b) C ((a' ^ b') v (a' ^ b))
9589, 94com2or 483 . . . . . . . 8 (a v b) C ((a ^ b) v ((a' ^ b') v (a' ^ b)))
9695, 91fh4 472 . . . . . . 7 (((a ^ b) v ((a' ^ b') v (a' ^ b))) v ((a v b) ^ b')) = ((((a ^ b) v ((a' ^ b') v (a' ^ b))) v (a v b)) ^ (((a ^ b) v ((a' ^ b') v (a' ^ b))) v b'))
97 or32 82 . . . . . . . . . 10 (((a ^ b) v ((a' ^ b') v (a' ^ b))) v (a v b)) = (((a ^ b) v (a v b)) v ((a' ^ b') v (a' ^ b)))
98 ax-a3 32 . . . . . . . . . . . . 13 (((a ^ b) v (a v b)) v (a' ^ b')) = ((a ^ b) v ((a v b) v (a' ^ b')))
99 anor3 90 . . . . . . . . . . . . . . . . 17 (a' ^ b') = (a v b)'
10099lor 70 . . . . . . . . . . . . . . . 16 ((a v b) v (a' ^ b')) = ((a v b) v (a v b)')
101 df-t 41 . . . . . . . . . . . . . . . . 17 1 = ((a v b) v (a v b)')
102101ax-r1 35 . . . . . . . . . . . . . . . 16 ((a v b) v (a v b)') = 1
103100, 102ax-r2 36 . . . . . . . . . . . . . . 15 ((a v b) v (a' ^ b')) = 1
104103lor 70 . . . . . . . . . . . . . 14 ((a ^ b) v ((a v b) v (a' ^ b'))) = ((a ^ b) v 1)
105 or1 104 . . . . . . . . . . . . . 14 ((a ^ b) v 1) = 1
106104, 105ax-r2 36 . . . . . . . . . . . . 13 ((a ^ b) v ((a v b) v (a' ^ b'))) = 1
10798, 106ax-r2 36 . . . . . . . . . . . 12 (((a ^ b) v (a v b)) v (a' ^ b')) = 1
108107ax-r5 38 . . . . . . . . . . 11 ((((a ^ b) v (a v b)) v (a' ^ b')) v (a' ^ b)) = (1 v (a' ^ b))
109 ax-a3 32 . . . . . . . . . . 11 ((((a ^ b) v (a v b)) v (a' ^ b')) v (a' ^ b)) = (((a ^ b) v (a v b)) v ((a' ^ b') v (a' ^ b)))
110 ax-a2 31 . . . . . . . . . . . 12 (1 v (a' ^ b)) = ((a' ^ b) v 1)
111 or1 104 . . . . . . . . . . . 12 ((a' ^ b) v 1) = 1
112110, 111ax-r2 36 . . . . . . . . . . 11 (1 v (a' ^ b)) = 1
113108, 109, 1123tr2 64 . . . . . . . . . 10 (((a ^ b) v (a v b)) v ((a' ^ b') v (a' ^ b))) = 1
11497, 113ax-r2 36 . . . . . . . . 9 (((a ^ b) v ((a' ^ b') v (a' ^ b))) v (a v b)) = 1
115 or12 80 . . . . . . . . . . 11 ((a ^ b) v ((a' ^ b') v (a' ^ b))) = ((a' ^ b') v ((a ^ b) v (a' ^ b)))
116115ax-r5 38 . . . . . . . . . 10 (((a ^ b) v ((a' ^ b') v (a' ^ b))) v b') = (((a' ^ b') v ((a ^ b) v (a' ^ b))) v b')
117 lear 161 . . . . . . . . . . . . 13 (a' ^ b') =< b'
118117df-le2 131 . . . . . . . . . . . 12 ((a' ^ b') v b') = b'
119118ax-r5 38 . . . . . . . . . . 11 (((a' ^ b') v b') v ((a ^ b) v (a' ^ b))) = (b' v ((a ^ b) v (a' ^ b)))
120 or32 82 . . . . . . . . . . 11 (((a' ^ b') v ((a ^ b) v (a' ^ b))) v b') = (((a' ^ b') v b') v ((a ^ b) v (a' ^ b)))
121 id 59 . . . . . . . . . . 11 (b' v ((a ^ b) v (a' ^ b))) = (b' v ((a ^ b) v (a' ^ b)))
122119, 120, 1213tr1 63 . . . . . . . . . 10 (((a' ^ b') v ((a ^ b) v (a' ^ b))) v b') = (b' v ((a ^ b) v (a' ^ b)))
123116, 122ax-r2 36 . . . . . . . . 9 (((a ^ b) v ((a' ^ b') v (a' ^ b))) v b') = (b' v ((a ^ b) v (a' ^ b)))
124114, 1232an 79 . . . . . . . 8 ((((a ^ b) v ((a' ^ b') v (a' ^ b))) v (a v b)) ^ (((a ^ b) v ((a' ^ b') v (a' ^ b))) v b')) = (1 ^ (b' v ((a ^ b) v (a' ^ b))))
125 ancom 74 . . . . . . . . 9 (1 ^ (b' v ((a ^ b) v (a' ^ b)))) = ((b' v ((a ^ b) v (a' ^ b))) ^ 1)
126 an1 106 . . . . . . . . 9 ((b' v ((a ^ b) v (a' ^ b))) ^ 1) = (b' v ((a ^ b) v (a' ^ b)))
127125, 126ax-r2 36 . . . . . . . 8 (1 ^ (b' v ((a ^ b) v (a' ^ b)))) = (b' v ((a ^ b) v (a' ^ b)))
128124, 127ax-r2 36 . . . . . . 7 ((((a ^ b) v ((a' ^ b') v (a' ^ b))) v (a v b)) ^ (((a ^ b) v ((a' ^ b') v (a' ^ b))) v b')) = (b' v ((a ^ b) v (a' ^ b)))
12996, 128ax-r2 36 . . . . . 6 (((a ^ b) v ((a' ^ b') v (a' ^ b))) v ((a v b) ^ b')) = (b' v ((a ^ b) v (a' ^ b)))
13086, 1292an 79 . . . . 5 ((((a ^ b) v ((a' ^ b') v (a' ^ b))) v (a' v b)) ^ (((a ^ b) v ((a' ^ b') v (a' ^ b))) v ((a v b) ^ b'))) = ((a' v b) ^ (b' v ((a ^ b) v (a' ^ b))))
131 comorr2 463 . . . . . . . 8 b C (a' v b)
132131comcom3 454 . . . . . . 7 b' C (a' v b)
133 comanr2 465 . . . . . . . . 9 b C (a ^ b)
134 comanr2 465 . . . . . . . . 9 b C (a' ^ b)
135133, 134com2or 483 . . . . . . . 8 b C ((a ^ b) v (a' ^ b))
136135comcom3 454 . . . . . . 7 b' C ((a ^ b) v (a' ^ b))
137132, 136fh2 470 . . . . . 6 ((a' v b) ^ (b' v ((a ^ b) v (a' ^ b)))) = (((a' v b) ^ b') v ((a' v b) ^ ((a ^ b) v (a' ^ b))))
138 ax-a2 31 . . . . . . 7 (((a' v b) ^ b') v ((a ^ b) v (a' ^ b))) = (((a ^ b) v (a' ^ b)) v ((a' v b) ^ b'))
139 ancom 74 . . . . . . . . 9 ((a' v b) ^ ((a ^ b) v (a' ^ b))) = (((a ^ b) v (a' ^ b)) ^ (a' v b))
140 lear 161 . . . . . . . . . . . 12 (a' ^ b) =< b
14177, 140lel2or 170 . . . . . . . . . . 11 ((a ^ b) v (a' ^ b)) =< b
142141, 78letr 137 . . . . . . . . . 10 ((a ^ b) v (a' ^ b)) =< (a' v b)
143142df2le2 136 . . . . . . . . 9 (((a ^ b) v (a' ^ b)) ^ (a' v b)) = ((a ^ b) v (a' ^ b))
144139, 143ax-r2 36 . . . . . . . 8 ((a' v b) ^ ((a ^ b) v (a' ^ b))) = ((a ^ b) v (a' ^ b))
145144lor 70 . . . . . . 7 (((a' v b) ^ b') v ((a' v b) ^ ((a ^ b) v (a' ^ b)))) = (((a' v b) ^ b') v ((a ^ b) v (a' ^ b)))
146 df-i4 47 . . . . . . 7 (a ->4 b) = (((a ^ b) v (a' ^ b)) v ((a' v b) ^ b'))
147138, 145, 1463tr1 63 . . . . . 6 (((a' v b) ^ b') v ((a' v b) ^ ((a ^ b) v (a' ^ b)))) = (a ->4 b)
148137, 147ax-r2 36 . . . . 5 ((a' v b) ^ (b' v ((a ^ b) v (a' ^ b)))) = (a ->4 b)
149130, 148ax-r2 36 . . . 4 ((((a ^ b) v ((a' ^ b') v (a' ^ b))) v (a' v b)) ^ (((a ^ b) v ((a' ^ b') v (a' ^ b))) v ((a v b) ^ b'))) = (a ->4 b)
15076, 149ax-r2 36 . . 3 (((a ^ b) v ((a' ^ b') v (a' ^ b))) v ((a' v b) ^ ((a v b) ^ b'))) = (a ->4 b)
15167, 150ax-r2 36 . 2 (((a ^ (a ->4 (a ->4 b))) v (a' ^ (a ->4 (a ->4 b)))) v ((a' v (a ->4 (a ->4 b))) ^ (a ->4 (a ->4 b))')) = (a ->4 b)
1521, 151ax-r2 36 1 (a ->4 (a ->4 (a ->4 b))) = (a ->4 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: (None)
  Copyright terms: Public domain W3C validator