QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  u3lem13b Unicode version
Theorem u3lem13b 790
Description: Lemma for unified implication study.
Assertion
Ref Expression
u3lem13b ((a ->3 b') ->3 a') = (a ->1 b)
Proof of Theorem u3lem13b
StepHypRef Expression
1 df-i3 46 . 2 ((a ->3 b') ->3 a') = ((((a ->3 b')' ^ a') v ((a ->3 b')' ^ a'')) v ((a ->3 b') ^ ((a ->3 b')' v a')))
2 u3lemnana 647 . . . . . 6 ((a ->3 b')' ^ a') = (a' ^ ((a v b') ^ (a v b'')))
3 ax-a1 30 . . . . . . . . 9 a = a''
43ax-r1 35 . . . . . . . 8 a'' = a
54lan 77 . . . . . . 7 ((a ->3 b')' ^ a'') = ((a ->3 b')' ^ a)
6 u3lemnaa 642 . . . . . . 7 ((a ->3 b')' ^ a) = (a ^ b'')
75, 6ax-r2 36 . . . . . 6 ((a ->3 b')' ^ a'') = (a ^ b'')
82, 72or 72 . . . . 5 (((a ->3 b')' ^ a') v ((a ->3 b')' ^ a'')) = ((a' ^ ((a v b') ^ (a v b''))) v (a ^ b''))
9 comanr1 464 . . . . . . . 8 a C (a ^ b'')
109comcom3 454 . . . . . . 7 a' C (a ^ b'')
11 comorr 184 . . . . . . . . 9 a C (a v b')
12 comorr 184 . . . . . . . . 9 a C (a v b'')
1311, 12com2an 484 . . . . . . . 8 a C ((a v b') ^ (a v b''))
1413comcom3 454 . . . . . . 7 a' C ((a v b') ^ (a v b''))
1510, 14fh4r 476 . . . . . 6 ((a' ^ ((a v b') ^ (a v b''))) v (a ^ b'')) = ((a' v (a ^ b'')) ^ (((a v b') ^ (a v b'')) v (a ^ b'')))
16 coman1 185 . . . . . . . . . 10 (a ^ b'') C a
17 coman2 186 . . . . . . . . . . 11 (a ^ b'') C b''
1817comcom7 460 . . . . . . . . . 10 (a ^ b'') C b'
1916, 18com2or 483 . . . . . . . . 9 (a ^ b'') C (a v b')
2016, 17com2or 483 . . . . . . . . 9 (a ^ b'') C (a v b'')
2119, 20fh3r 475 . . . . . . . 8 (((a v b') ^ (a v b'')) v (a ^ b'')) = (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b'')))
2221lan 77 . . . . . . 7 ((a' v (a ^ b'')) ^ (((a v b') ^ (a v b'')) v (a ^ b''))) = ((a' v (a ^ b'')) ^ (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b''))))
23 ax-a2 31 . . . . . . . . . . . 12 ((a v b') v (a ^ b'')) = ((a ^ b'') v (a v b'))
24 lea 160 . . . . . . . . . . . . . 14 (a ^ b'') =< a
25 leo 158 . . . . . . . . . . . . . 14 a =< (a v b')
2624, 25letr 137 . . . . . . . . . . . . 13 (a ^ b'') =< (a v b')
2726df-le2 131 . . . . . . . . . . . 12 ((a ^ b'') v (a v b')) = (a v b')
2823, 27ax-r2 36 . . . . . . . . . . 11 ((a v b') v (a ^ b'')) = (a v b')
29 ax-a2 31 . . . . . . . . . . . 12 ((a v b'') v (a ^ b'')) = ((a ^ b'') v (a v b''))
30 leo 158 . . . . . . . . . . . . . 14 a =< (a v b'')
3124, 30letr 137 . . . . . . . . . . . . 13 (a ^ b'') =< (a v b'')
3231df-le2 131 . . . . . . . . . . . 12 ((a ^ b'') v (a v b'')) = (a v b'')
3329, 32ax-r2 36 . . . . . . . . . . 11 ((a v b'') v (a ^ b'')) = (a v b'')
3428, 332an 79 . . . . . . . . . 10 (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b''))) = ((a v b') ^ (a v b''))
35 id 59 . . . . . . . . . 10 ((a v b') ^ (a v b'')) = ((a v b') ^ (a v b''))
3634, 35ax-r2 36 . . . . . . . . 9 (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b''))) = ((a v b') ^ (a v b''))
3736lan 77 . . . . . . . 8 ((a' v (a ^ b'')) ^ (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b'')))) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
38 id 59 . . . . . . . 8 ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b''))) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
3937, 38ax-r2 36 . . . . . . 7 ((a' v (a ^ b'')) ^ (((a v b') v (a ^ b'')) ^ ((a v b'') v (a ^ b'')))) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
4022, 39ax-r2 36 . . . . . 6 ((a' v (a ^ b'')) ^ (((a v b') ^ (a v b'')) v (a ^ b''))) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
4115, 40ax-r2 36 . . . . 5 ((a' ^ ((a v b') ^ (a v b''))) v (a ^ b'')) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
428, 41ax-r2 36 . . . 4 (((a ->3 b')' ^ a') v ((a ->3 b')' ^ a'')) = ((a' v (a ^ b'')) ^ ((a v b') ^ (a v b'')))
43 u3lemnona 667 . . . . . 6 ((a ->3 b')' v a') = (a' v (a ^ b''))
4443lan 77 . . . . 5 ((a ->3 b') ^ ((a ->3 b')' v a')) = ((a ->3 b') ^ (a' v (a ^ b'')))
45 comi31 508 . . . . . . . 8 a C (a ->3 b')
4645comcom3 454 . . . . . . 7 a' C (a ->3 b')
4746, 10fh2 470 . . . . . 6 ((a ->3 b') ^ (a' v (a ^ b''))) = (((a ->3 b') ^ a') v ((a ->3 b') ^ (a ^ b'')))
48 u3lemana 607 . . . . . . . 8 ((a ->3 b') ^ a') = ((a' ^ b') v (a' ^ b''))
49 anandi 114 . . . . . . . . 9 ((a ->3 b') ^ (a ^ b'')) = (((a ->3 b') ^ a) ^ ((a ->3 b') ^ b''))
50 u3lemaa 602 . . . . . . . . . . 11 ((a ->3 b') ^ a) = (a ^ (a' v b'))
51 u3lemanb 617 . . . . . . . . . . 11 ((a ->3 b') ^ b'') = (a' ^ b'')
5250, 512an 79 . . . . . . . . . 10 (((a ->3 b') ^ a) ^ ((a ->3 b') ^ b'')) = ((a ^ (a' v b')) ^ (a' ^ b''))
53 an4 86 . . . . . . . . . . 11 ((a ^ (a' v b')) ^ (a' ^ b'')) = ((a ^ a') ^ ((a' v b') ^ b''))
54 ancom 74 . . . . . . . . . . . 12 ((a ^ a') ^ ((a' v b') ^ b'')) = (((a' v b') ^ b'') ^ (a ^ a'))
55 dff 101 . . . . . . . . . . . . . . 15 0 = (a ^ a')
5655ax-r1 35 . . . . . . . . . . . . . 14 (a ^ a') = 0
5756lan 77 . . . . . . . . . . . . 13 (((a' v b') ^ b'') ^ (a ^ a')) = (((a' v b') ^ b'') ^ 0)
58 an0 108 . . . . . . . . . . . . 13 (((a' v b') ^ b'') ^ 0) = 0
5957, 58ax-r2 36 . . . . . . . . . . . 12 (((a' v b') ^ b'') ^ (a ^ a')) = 0
6054, 59ax-r2 36 . . . . . . . . . . 11 ((a ^ a') ^ ((a' v b') ^ b'')) = 0
6153, 60ax-r2 36 . . . . . . . . . 10 ((a ^ (a' v b')) ^ (a' ^ b'')) = 0
6252, 61ax-r2 36 . . . . . . . . 9 (((a ->3 b') ^ a) ^ ((a ->3 b') ^ b'')) = 0
6349, 62ax-r2 36 . . . . . . . 8 ((a ->3 b') ^ (a ^ b'')) = 0
6448, 632or 72 . . . . . . 7 (((a ->3 b') ^ a') v ((a ->3 b') ^ (a ^ b''))) = (((a' ^ b') v (a' ^ b'')) v 0)
65 or0 102 . . . . . . 7 (((a' ^ b') v (a' ^ b'')) v 0) = ((a' ^ b') v (a' ^ b''))
6664, 65ax-r2 36 . . . . . 6 (((a ->3 b') ^ a') v ((a ->3 b') ^ (a ^ b''))) = ((a' ^ b') v (a' ^ b''))
6747, 66ax-r2 36 . . . . 5 ((a ->3 b') ^ (a' v (a ^ b''))) = ((a' ^ b') v (a' ^ b''))
6844, 67ax-r2 36 . . . 4 ((a ->3 b') ^ ((a ->3 b')' v a')) = ((a' ^ b') v (a' ^ b''))
6942, 682or 72 . . 3 ((((a ->3 b')' ^ a') v ((a ->3 b')' ^ a'')) v ((a ->3 b') ^ ((a ->3 b')' v a'))) = (((a' v (a ^ b'')) ^ ((a v b') ^ (a v b''))) v ((a' ^ b') v (a' ^ b'')))
70 comanr1 464 . . . . . . . . 9 a' C (a' ^ b')
71 comanr1 464 . . . . . . . . 9 a' C (a' ^ b'')
7270, 71com2or 483 . . . . . . . 8 a' C ((a' ^ b') v (a' ^ b''))
7372comcom 453 . . . . . . 7 ((a' ^ b') v (a' ^ b'')) C a'
7473comcom7 460 . . . . . . . 8 ((a' ^ b') v (a' ^ b'')) C a
75 comanr2 465 . . . . . . . . . . 11 b' C (a' ^ b')
7675comcom3 454 . . . . . . . . . 10 b'' C (a' ^ b')
77 comanr2 465 . . . . . . . . . 10 b'' C (a' ^ b'')
7876, 77com2or 483 . . . . . . . . 9 b'' C ((a' ^ b') v (a' ^ b''))
7978comcom 453 . . . . . . . 8 ((a' ^ b') v (a' ^ b'')) C b''
8074, 79com2an 484 . . . . . . 7 ((a' ^ b') v (a' ^ b'')) C (a ^ b'')
8173, 80com2or 483 . . . . . 6 ((a' ^ b') v (a' ^ b'')) C (a' v (a ^ b''))
8281comcom 453 . . . . 5 (a' v (a ^ b'')) C ((a' ^ b') v (a' ^ b''))
8313comcom 453 . . . . . . . 8 ((a v b') ^ (a v b'')) C a
8483comcom2 183 . . . . . . 7 ((a v b') ^ (a v b'')) C a'
85 comorr2 463 . . . . . . . . . . 11 b' C (a v b')
8685comcom3 454 . . . . . . . . . 10 b'' C (a v b')
87 comorr2 463 . . . . . . . . . 10 b'' C (a v b'')
8886, 87com2an 484 . . . . . . . . 9 b'' C ((a v b') ^ (a v b''))
8988comcom 453 . . . . . . . 8 ((a v b') ^ (a v b'')) C b''
9083, 89com2an 484 . . . . . . 7 ((a v b') ^ (a v b'')) C (a ^ b'')
9184, 90com2or 483 . . . . . 6 ((a v b') ^ (a v b'')) C (a' v (a ^ b''))
9291comcom 453 . . . . 5 (a' v (a ^ b'')) C ((a v b') ^ (a v b''))
9382, 92fh4r 476 . . . 4 (((a' v (a ^ b'')) ^ ((a v b') ^ (a v b''))) v ((a' ^ b') v (a' ^ b''))) = (((a' v (a ^ b'')) v ((a' ^ b') v (a' ^ b''))) ^ (((a v b') ^ (a v b'')) v ((a' ^ b') v (a' ^ b''))))
94 ax-a2 31 . . . . . . 7 ((a' v (a ^ b'')) v ((a' ^ b') v (a' ^ b''))) = (((a' ^ b') v (a' ^ b'')) v (a' v (a ^ b'')))
95 lea 160 . . . . . . . . . . 11 (a' ^ b') =< a'
96 lea 160 . . . . . . . . . . 11 (a' ^ b'') =< a'
9795, 96lel2or 170 . . . . . . . . . 10 ((a' ^ b') v (a' ^ b'')) =< a'
98 leo 158 . . . . . . . . . 10 a' =< (a' v (a ^ b''))
9997, 98letr 137 . . . . . . . . 9 ((a' ^ b') v (a' ^ b'')) =< (a' v (a ^ b''))
10099df-le2 131 . . . . . . . 8 (((a' ^ b') v (a' ^ b'')) v (a' v (a ^ b''))) = (a' v (a ^ b''))
101 id 59 . . . . . . . 8 (a' v (a ^ b'')) = (a' v (a ^ b''))
102100, 101ax-r2 36 . . . . . . 7 (((a' ^ b') v (a' ^ b'')) v (a' v (a ^ b''))) = (a' v (a ^ b''))
10394, 102ax-r2 36 . . . . . 6 ((a' v (a ^ b'')) v ((a' ^ b') v (a' ^ b''))) = (a' v (a ^ b''))
104 ax-a2 31 . . . . . . . . 9 ((a' ^ b') v (a' ^ b'')) = ((a' ^ b'') v (a' ^ b'))
105 anor3 90 . . . . . . . . . . 11 (a' ^ b'') = (a v b')'
106 anor2 89 . . . . . . . . . . 11 (a' ^ b') = (a v b'')'
107105, 1062or 72 . . . . . . . . . 10 ((a' ^ b'') v (a' ^ b')) = ((a v b')' v (a v b'')')
108 oran3 93 . . . . . . . . . 10 ((a v b')' v (a v b'')') = ((a v b') ^ (a v b''))'
109107, 108ax-r2 36 . . . . . . . . 9 ((a' ^ b'') v (a' ^ b')) = ((a v b') ^ (a v b''))'
110104, 109ax-r2 36 . . . . . . . 8 ((a' ^ b') v (a' ^ b'')) = ((a v b') ^ (a v b''))'
111110lor 70 . . . . . . 7 (((a v b') ^ (a v b'')) v ((a' ^ b') v (a' ^ b''))) = (((a v b') ^ (a v b'')) v ((a v b') ^ (a v b''))')
112 df-t 41 . . . . . . . 8 1 = (((a v b') ^ (a v b'')) v ((a v b') ^ (a v b''))')
113112ax-r1 35 . . . . . . 7 (((a v b') ^ (a v b'')) v ((a v b') ^ (a v b''))') = 1
114111, 113ax-r2 36 . . . . . 6 (((a v b') ^ (a v b'')) v ((a' ^ b') v (a' ^ b''))) = 1
115103, 1142an 79 . . . . 5 (((a' v (a ^ b'')) v ((a' ^ b') v (a' ^ b''))) ^ (((a v b') ^ (a v b'')) v ((a' ^ b') v (a' ^ b'')))) = ((a' v (a ^ b'')) ^ 1)
116 an1 106 . . . . . 6 ((a' v (a ^ b'')) ^ 1) = (a' v (a ^ b''))
117 df-i1 44 . . . . . . . 8 (a ->1 b'') = (a' v (a ^ b''))
118117ax-r1 35 . . . . . . 7 (a' v (a ^ b'')) = (a ->1 b'')
119 ax-a1 30 . . . . . . . . 9 b = b''
120119ax-r1 35 . . . . . . . 8 b'' = b
121120ud1lem0a 255 . . . . . . 7 (a ->1 b'') = (a ->1 b)
122118, 121ax-r2 36 . . . . . 6 (a' v (a ^ b'')) = (a ->1 b)
123116, 122ax-r2 36 . . . . 5 ((a' v (a ^ b'')) ^ 1) = (a ->1 b)
124115, 123ax-r2 36 . . . 4 (((a' v (a ^ b'')) v ((a' ^ b') v (a' ^ b''))) ^ (((a v b') ^ (a v b'')) v ((a' ^ b') v (a' ^ b'')))) = (a ->1 b)
12593, 124ax-r2 36 . . 3 (((a' v (a ^ b'')) ^ ((a v b') ^ (a v b''))) v ((a' ^ b') v (a' ^ b''))) = (a ->1 b)
12669, 125ax-r2 36 . 2 ((((a ->3 b')' ^ a') v ((a ->3 b')' ^ a'')) v ((a ->3 b') ^ ((a ->3 b')' v a'))) = (a ->1 b)
1271, 126ax-r2 36 1 ((a ->3 b') ->3 a') = (a ->1 b)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8  0wf 9   ->1 wi1 12   ->3 wi3 14
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-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  u3lem14a  791  u3lem14aa2  793
  Copyright terms: Public domain W3C validator