QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  vneulemexp Unicode version

Theorem vneulemexp 1146
Description: Expanded version of vneulem 1145.
Hypothesis
Ref Expression
vneulemexp.1 ((a v b) ^ (c v d)) = 0
Assertion
Ref Expression
vneulemexp ((a v c) ^ (b v d)) = ((a ^ b) v (c ^ d))

Proof of Theorem vneulemexp
StepHypRef Expression
1 ax-a2 31 . . . . . . 7 (a v b) = (b v a)
21ax-r5 38 . . . . . 6 ((a v b) v c) = ((b v a) v c)
3 or32 82 . . . . . 6 ((a v c) v d) = ((a v d) v c)
42, 32an 79 . . . . 5 (((a v b) v c) ^ ((a v c) v d)) = (((b v a) v c) ^ ((a v d) v c))
5 orcom 73 . . . . . . . . . . . 12 (b v a) = (a v b)
65ror 71 . . . . . . . . . . 11 ((b v a) v c) = ((a v b) v c)
7 or32 82 . . . . . . . . . . 11 ((a v b) v c) = ((a v c) v b)
86, 7tr 62 . . . . . . . . . 10 ((b v a) v c) = ((a v c) v b)
9 or32 82 . . . . . . . . . 10 ((a v d) v c) = ((a v c) v d)
108, 92an 79 . . . . . . . . 9 (((b v a) v c) ^ ((a v d) v c)) = (((a v c) v b) ^ ((a v c) v d))
11 ancom 74 . . . . . . . . . 10 (((a v c) v b) ^ ((a v c) v d)) = (((a v c) v d) ^ ((a v c) v b))
12 ml 1121 . . . . . . . . . . 11 ((a v c) v (d ^ ((a v c) v b))) = (((a v c) v d) ^ ((a v c) v b))
1312cm 61 . . . . . . . . . 10 (((a v c) v d) ^ ((a v c) v b)) = ((a v c) v (d ^ ((a v c) v b)))
14 ancom 74 . . . . . . . . . . 11 (d ^ ((a v c) v b)) = (((a v c) v b) ^ d)
1514lor 70 . . . . . . . . . 10 ((a v c) v (d ^ ((a v c) v b))) = ((a v c) v (((a v c) v b) ^ d))
1611, 13, 153tr 65 . . . . . . . . 9 (((a v c) v b) ^ ((a v c) v d)) = ((a v c) v (((a v c) v b) ^ d))
1710, 16ax-r2 36 . . . . . . . 8 (((b v a) v c) ^ ((a v d) v c)) = ((a v c) v (((a v c) v b) ^ d))
18 leor 159 . . . . . . . . 9 (a v c) =< ((d ^ b) v (a v c))
19 or32 82 . . . . . . . . . . . 12 ((a v c) v b) = ((a v b) v c)
2019ran 78 . . . . . . . . . . 11 (((a v c) v b) ^ d) = (((a v b) v c) ^ d)
21 leor 159 . . . . . . . . . . . . . . 15 d =< (c v d)
22 leid 148 . . . . . . . . . . . . . . 15 d =< d
2321, 22ler2an 173 . . . . . . . . . . . . . 14 d =< ((c v d) ^ d)
24 lear 161 . . . . . . . . . . . . . 14 ((c v d) ^ d) =< d
2523, 24lebi 145 . . . . . . . . . . . . 13 d = ((c v d) ^ d)
2625lan 77 . . . . . . . . . . . 12 (((a v b) v c) ^ d) = (((a v b) v c) ^ ((c v d) ^ d))
27 anass 76 . . . . . . . . . . . . . 14 ((((a v b) v c) ^ (c v d)) ^ d) = (((a v b) v c) ^ ((c v d) ^ d))
2827cm 61 . . . . . . . . . . . . 13 (((a v b) v c) ^ ((c v d) ^ d)) = ((((a v b) v c) ^ (c v d)) ^ d)
29 ax-a2 31 . . . . . . . . . . . . . . . 16 ((a v b) v c) = (c v (a v b))
3029ran 78 . . . . . . . . . . . . . . 15 (((a v b) v c) ^ (c v d)) = ((c v (a v b)) ^ (c v d))
31 ml 1121 . . . . . . . . . . . . . . . 16 (c v ((a v b) ^ (c v d))) = ((c v (a v b)) ^ (c v d))
3231cm 61 . . . . . . . . . . . . . . 15 ((c v (a v b)) ^ (c v d)) = (c v ((a v b) ^ (c v d)))
33 orcom 73 . . . . . . . . . . . . . . 15 (c v ((a v b) ^ (c v d))) = (((a v b) ^ (c v d)) v c)
3430, 32, 333tr 65 . . . . . . . . . . . . . 14 (((a v b) v c) ^ (c v d)) = (((a v b) ^ (c v d)) v c)
3534ran 78 . . . . . . . . . . . . 13 ((((a v b) v c) ^ (c v d)) ^ d) = ((((a v b) ^ (c v d)) v c) ^ d)
3628, 35tr 62 . . . . . . . . . . . 12 (((a v b) v c) ^ ((c v d) ^ d)) = ((((a v b) ^ (c v d)) v c) ^ d)
37 vneulemexp.1 . . . . . . . . . . . . . . 15 ((a v b) ^ (c v d)) = 0
3837ror 71 . . . . . . . . . . . . . 14 (((a v b) ^ (c v d)) v c) = (0 v c)
39 or0r 103 . . . . . . . . . . . . . 14 (0 v c) = c
4038, 39tr 62 . . . . . . . . . . . . 13 (((a v b) ^ (c v d)) v c) = c
4140ran 78 . . . . . . . . . . . 12 ((((a v b) ^ (c v d)) v c) ^ d) = (c ^ d)
4226, 36, 413tr 65 . . . . . . . . . . 11 (((a v b) v c) ^ d) = (c ^ d)
4320, 42tr 62 . . . . . . . . . 10 (((a v c) v b) ^ d) = (c ^ d)
44 leao3 164 . . . . . . . . . . 11 (c ^ d) =< (a v c)
4544lerr 150 . . . . . . . . . 10 (c ^ d) =< ((d ^ b) v (a v c))
4643, 45bltr 138 . . . . . . . . 9 (((a v c) v b) ^ d) =< ((d ^ b) v (a v c))
4718, 46lel2or 170 . . . . . . . 8 ((a v c) v (((a v c) v b) ^ d)) =< ((d ^ b) v (a v c))
4817, 47bltr 138 . . . . . . 7 (((b v a) v c) ^ ((a v d) v c)) =< ((d ^ b) v (a v c))
49 leao2 163 . . . . . . . . . 10 (d ^ b) =< (b v a)
5049ler 149 . . . . . . . . 9 (d ^ b) =< ((b v a) v c)
51 leor 159 . . . . . . . . . 10 a =< (b v a)
5251leror 152 . . . . . . . . 9 (a v c) =< ((b v a) v c)
5350, 52lel2or 170 . . . . . . . 8 ((d ^ b) v (a v c)) =< ((b v a) v c)
54 leao3 164 . . . . . . . . . 10 (d ^ b) =< (a v d)
5554ler 149 . . . . . . . . 9 (d ^ b) =< ((a v d) v c)
56 leo 158 . . . . . . . . . 10 a =< (a v d)
5756leror 152 . . . . . . . . 9 (a v c) =< ((a v d) v c)
5855, 57lel2or 170 . . . . . . . 8 ((d ^ b) v (a v c)) =< ((a v d) v c)
5953, 58ler2an 173 . . . . . . 7 ((d ^ b) v (a v c)) =< (((b v a) v c) ^ ((a v d) v c))
6048, 59lebi 145 . . . . . 6 (((b v a) v c) ^ ((a v d) v c)) = ((d ^ b) v (a v c))
61 leao1 162 . . . . . . . . . . 11 (d ^ b) =< (d v c)
6249, 61ler2an 173 . . . . . . . . . 10 (d ^ b) =< ((b v a) ^ (d v c))
63 orcom 73 . . . . . . . . . . . 12 (d v c) = (c v d)
645, 632an 79 . . . . . . . . . . 11 ((b v a) ^ (d v c)) = ((a v b) ^ (c v d))
6564, 37tr 62 . . . . . . . . . 10 ((b v a) ^ (d v c)) = 0
6662, 65lbtr 139 . . . . . . . . 9 (d ^ b) =< 0
67 le0 147 . . . . . . . . 9 0 =< (d ^ b)
6866, 67lebi 145 . . . . . . . 8 (d ^ b) = 0
6968ror 71 . . . . . . 7 ((d ^ b) v (a v c)) = (0 v (a v c))
70 or0r 103 . . . . . . 7 (0 v (a v c)) = (a v c)
7169, 70tr 62 . . . . . 6 ((d ^ b) v (a v c)) = (a v c)
7260, 71tr 62 . . . . 5 (((b v a) v c) ^ ((a v d) v c)) = (a v c)
734, 72tr 62 . . . 4 (((a v b) v c) ^ ((a v c) v d)) = (a v c)
74 orcom 73 . . . . . . . . . . 11 (a v b) = (b v a)
7574ror 71 . . . . . . . . . 10 ((a v b) v d) = ((b v a) v d)
76 or32 82 . . . . . . . . . 10 ((b v a) v d) = ((b v d) v a)
7775, 76tr 62 . . . . . . . . 9 ((a v b) v d) = ((b v d) v a)
78 or32 82 . . . . . . . . 9 ((b v c) v d) = ((b v d) v c)
7977, 782an 79 . . . . . . . 8 (((a v b) v d) ^ ((b v c) v d)) = (((b v d) v a) ^ ((b v d) v c))
80 ancom 74 . . . . . . . . 9 (((b v d) v a) ^ ((b v d) v c)) = (((b v d) v c) ^ ((b v d) v a))
81 ml 1121 . . . . . . . . . 10 ((b v d) v (c ^ ((b v d) v a))) = (((b v d) v c) ^ ((b v d) v a))
8281cm 61 . . . . . . . . 9 (((b v d) v c) ^ ((b v d) v a)) = ((b v d) v (c ^ ((b v d) v a)))
83 ancom 74 . . . . . . . . . 10 (c ^ ((b v d) v a)) = (((b v d) v a) ^ c)
8483lor 70 . . . . . . . . 9 ((b v d) v (c ^ ((b v d) v a))) = ((b v d) v (((b v d) v a) ^ c))
8580, 82, 843tr 65 . . . . . . . 8 (((b v d) v a) ^ ((b v d) v c)) = ((b v d) v (((b v d) v a) ^ c))
8679, 85ax-r2 36 . . . . . . 7 (((a v b) v d) ^ ((b v c) v d)) = ((b v d) v (((b v d) v a) ^ c))
87 leor 159 . . . . . . . 8 (b v d) =< ((c ^ a) v (b v d))
88 or32 82 . . . . . . . . . . 11 ((b v d) v a) = ((b v a) v d)
8988ran 78 . . . . . . . . . 10 (((b v d) v a) ^ c) = (((b v a) v d) ^ c)
90 leor 159 . . . . . . . . . . . . . 14 c =< (d v c)
91 leid 148 . . . . . . . . . . . . . 14 c =< c
9290, 91ler2an 173 . . . . . . . . . . . . 13 c =< ((d v c) ^ c)
93 lear 161 . . . . . . . . . . . . 13 ((d v c) ^ c) =< c
9492, 93lebi 145 . . . . . . . . . . . 12 c = ((d v c) ^ c)
9594lan 77 . . . . . . . . . . 11 (((b v a) v d) ^ c) = (((b v a) v d) ^ ((d v c) ^ c))
96 anass 76 . . . . . . . . . . . . 13 ((((b v a) v d) ^ (d v c)) ^ c) = (((b v a) v d) ^ ((d v c) ^ c))
9796cm 61 . . . . . . . . . . . 12 (((b v a) v d) ^ ((d v c) ^ c)) = ((((b v a) v d) ^ (d v c)) ^ c)
98 ax-a2 31 . . . . . . . . . . . . . . 15 ((b v a) v d) = (d v (b v a))
9998ran 78 . . . . . . . . . . . . . 14 (((b v a) v d) ^ (d v c)) = ((d v (b v a)) ^ (d v c))
100 ml 1121 . . . . . . . . . . . . . . 15 (d v ((b v a) ^ (d v c))) = ((d v (b v a)) ^ (d v c))
101100cm 61 . . . . . . . . . . . . . 14 ((d v (b v a)) ^ (d v c)) = (d v ((b v a) ^ (d v c)))
102 orcom 73 . . . . . . . . . . . . . 14 (d v ((b v a) ^ (d v c))) = (((b v a) ^ (d v c)) v d)
10399, 101, 1023tr 65 . . . . . . . . . . . . 13 (((b v a) v d) ^ (d v c)) = (((b v a) ^ (d v c)) v d)
104103ran 78 . . . . . . . . . . . 12 ((((b v a) v d) ^ (d v c)) ^ c) = ((((b v a) ^ (d v c)) v d) ^ c)
10597, 104tr 62 . . . . . . . . . . 11 (((b v a) v d) ^ ((d v c) ^ c)) = ((((b v a) ^ (d v c)) v d) ^ c)
10665ror 71 . . . . . . . . . . . . 13 (((b v a) ^ (d v c)) v d) = (0 v d)
107 or0r 103 . . . . . . . . . . . . 13 (0 v d) = d
108106, 107tr 62 . . . . . . . . . . . 12 (((b v a) ^ (d v c)) v d) = d
109108ran 78 . . . . . . . . . . 11 ((((b v a) ^ (d v c)) v d) ^ c) = (d ^ c)
11095, 105, 1093tr 65 . . . . . . . . . 10 (((b v a) v d) ^ c) = (d ^ c)
11189, 110tr 62 . . . . . . . . 9 (((b v d) v a) ^ c) = (d ^ c)
112 leao3 164 . . . . . . . . . 10 (d ^ c) =< (b v d)
113112lerr 150 . . . . . . . . 9 (d ^ c) =< ((c ^ a) v (b v d))
114111, 113bltr 138 . . . . . . . 8 (((b v d) v a) ^ c) =< ((c ^ a) v (b v d))
11587, 114lel2or 170 . . . . . . 7 ((b v d) v (((b v d) v a) ^ c)) =< ((c ^ a) v (b v d))
11686, 115bltr 138 . . . . . 6 (((a v b) v d) ^ ((b v c) v d)) =< ((c ^ a) v (b v d))
117 leao2 163 . . . . . . . . 9 (c ^ a) =< (a v b)
118117ler 149 . . . . . . . 8 (c ^ a) =< ((a v b) v d)
119 leor 159 . . . . . . . . 9 b =< (a v b)
120119leror 152 . . . . . . . 8 (b v d) =< ((a v b) v d)
121118, 120lel2or 170 . . . . . . 7 ((c ^ a) v (b v d)) =< ((a v b) v d)
122 leao3 164 . . . . . . . . 9 (c ^ a) =< (b v c)
123122ler 149 . . . . . . . 8 (c ^ a) =< ((b v c) v d)
124 leo 158 . . . . . . . . 9 b =< (b v c)
125124leror 152 . . . . . . . 8 (b v d) =< ((b v c) v d)
126123, 125lel2or 170 . . . . . . 7 ((c ^ a) v (b v d)) =< ((b v c) v d)
127121, 126ler2an 173 . . . . . 6 ((c ^ a) v (b v d)) =< (((a v b) v d) ^ ((b v c) v d))
128116, 127lebi 145 . . . . 5 (((a v b) v d) ^ ((b v c) v d)) = ((c ^ a) v (b v d))
129 leao1 162 . . . . . . . . . 10 (c ^ a) =< (c v d)
130117, 129ler2an 173 . . . . . . . . 9 (c ^ a) =< ((a v b) ^ (c v d))
131130, 37lbtr 139 . . . . . . . 8 (c ^ a) =< 0
132 le0 147 . . . . . . . 8 0 =< (c ^ a)
133131, 132lebi 145 . . . . . . 7 (c ^ a) = 0
134133ror 71 . . . . . 6 ((c ^ a) v (b v d)) = (0 v (b v d))
135 or0r 103 . . . . . 6 (0 v (b v d)) = (b v d)
136134, 135tr 62 . . . . 5 ((c ^ a) v (b v d)) = (b v d)
137128, 136tr 62 . . . 4 (((a v b) v d) ^ ((b v c) v d)) = (b v d)
13873, 1372an 79 . . 3 ((((a v b) v c) ^ ((a v c) v d)) ^ (((a v b) v d) ^ ((b v c) v d))) = ((a v c) ^ (b v d))
139138cm 61 . 2 ((a v c) ^ (b v d)) = ((((a v b) v c) ^ ((a v c) v d)) ^ (((a v b) v d) ^ ((b v c) v d)))
140 ancom 74 . . 3 ((((a v b) v c) ^ ((a v c) v d)) ^ (((a v b) v d) ^ ((b v c) v d))) = ((((a v b) v d) ^ ((b v c) v d)) ^ (((a v b) v c) ^ ((a v c) v d)))
141 an4 86 . . . 4 ((((a v b) v d) ^ ((b v c) v d)) ^ (((a v b) v c) ^ ((a v c) v d))) = ((((a v b) v d) ^ ((a v b) v c)) ^ (((b v c) v d) ^ ((a v c) v d)))
142 ancom 74 . . . . . . 7 (((a v b) v d) ^ ((a v b) v c)) = (((a v b) v c) ^ ((a v b) v d))
143 ancom 74 . . . . . . . 8 (((a v b) v c) ^ ((a v b) v d)) = (((a v b) v d) ^ ((a v b) v c))
144 ml 1121 . . . . . . . . 9 ((a v b) v (d ^ ((a v b) v c))) = (((a v b) v d) ^ ((a v b) v c))
145144cm 61 . . . . . . . 8 (((a v b) v d) ^ ((a v b) v c)) = ((a v b) v (d ^ ((a v b) v c)))
146 ancom 74 . . . . . . . . 9 (d ^ ((a v b) v c)) = (((a v b) v c) ^ d)
147146lor 70 . . . . . . . 8 ((a v b) v (d ^ ((a v b) v c))) = ((a v b) v (((a v b) v c) ^ d))
148143, 145, 1473tr 65 . . . . . . 7 (((a v b) v c) ^ ((a v b) v d)) = ((a v b) v (((a v b) v c) ^ d))
149142, 148ax-r2 36 . . . . . 6 (((a v b) v d) ^ ((a v b) v c)) = ((a v b) v (((a v b) v c) ^ d))
150 orcom 73 . . . . . 6 ((a v b) v (((a v b) v c) ^ d)) = ((((a v b) v c) ^ d) v (a v b))
15142ror 71 . . . . . 6 ((((a v b) v c) ^ d) v (a v b)) = ((c ^ d) v (a v b))
152149, 150, 1513tr 65 . . . . 5 (((a v b) v d) ^ ((a v b) v c)) = ((c ^ d) v (a v b))
153 ax-a3 32 . . . . . . . 8 ((b v c) v d) = (b v (c v d))
154 orcom 73 . . . . . . . 8 (b v (c v d)) = ((c v d) v b)
155153, 154tr 62 . . . . . . 7 ((b v c) v d) = ((c v d) v b)
156 ax-a2 31 . . . . . . . . 9 (a v c) = (c v a)
157156ror 71 . . . . . . . 8 ((a v c) v d) = ((c v a) v d)
158 or32 82 . . . . . . . 8 ((c v a) v d) = ((c v d) v a)
159157, 158tr 62 . . . . . . 7 ((a v c) v d) = ((c v d) v a)
160155, 1592an 79 . . . . . 6 (((b v c) v d) ^ ((a v c) v d)) = (((c v d) v b) ^ ((c v d) v a))
161 ancom 74 . . . . . . . 8 (((c v d) v b) ^ ((c v d) v a)) = (((c v d) v a) ^ ((c v d) v b))
162 ancom 74 . . . . . . . . 9 (((c v d) v a) ^ ((c v d) v b)) = (((c v d) v b) ^ ((c v d) v a))
163 ml 1121 . . . . . . . . . 10 ((c v d) v (b ^ ((c v d) v a))) = (((c v d) v b) ^ ((c v d) v a))
164163cm 61 . . . . . . . . 9 (((c v d) v b) ^ ((c v d) v a)) = ((c v d) v (b ^ ((c v d) v a)))
165 ancom 74 . . . . . . . . . 10 (b ^ ((c v d) v a)) = (((c v d) v a) ^ b)
166165lor 70 . . . . . . . . 9 ((c v d) v (b ^ ((c v d) v a))) = ((c v d) v (((c v d) v a) ^ b))
167162, 164, 1663tr 65 . . . . . . . 8 (((c v d) v a) ^ ((c v d) v b)) = ((c v d) v (((c v d) v a) ^ b))
168161, 167ax-r2 36 . . . . . . 7 (((c v d) v b) ^ ((c v d) v a)) = ((c v d) v (((c v d) v a) ^ b))
169 orcom 73 . . . . . . 7 ((c v d) v (((c v d) v a) ^ b)) = ((((c v d) v a) ^ b) v (c v d))
170 leid 148 . . . . . . . . . . . 12 b =< b
171119, 170ler2an 173 . . . . . . . . . . 11 b =< ((a v b) ^ b)
172 lear 161 . . . . . . . . . . 11 ((a v b) ^ b) =< b
173171, 172lebi 145 . . . . . . . . . 10 b = ((a v b) ^ b)
174173lan 77 . . . . . . . . 9 (((c v d) v a) ^ b) = (((c v d) v a) ^ ((a v b) ^ b))
175 anass 76 . . . . . . . . . . 11 ((((c v d) v a) ^ (a v b)) ^ b) = (((c v d) v a) ^ ((a v b) ^ b))
176175cm 61 . . . . . . . . . 10 (((c v d) v a) ^ ((a v b) ^ b)) = ((((c v d) v a) ^ (a v b)) ^ b)
177 ax-a2 31 . . . . . . . . . . . . 13 ((c v d) v a) = (a v (c v d))
178177ran 78 . . . . . . . . . . . 12 (((c v d) v a) ^ (a v b)) = ((a v (c v d)) ^ (a v b))
179 ml 1121 . . . . . . . . . . . . 13 (a v ((c v d) ^ (a v b))) = ((a v (c v d)) ^ (a v b))
180179cm 61 . . . . . . . . . . . 12 ((a v (c v d)) ^ (a v b)) = (a v ((c v d) ^ (a v b)))
181 orcom 73 . . . . . . . . . . . 12 (a v ((c v d) ^ (a v b))) = (((c v d) ^ (a v b)) v a)
182178, 180, 1813tr 65 . . . . . . . . . . 11 (((c v d) v a) ^ (a v b)) = (((c v d) ^ (a v b)) v a)
183182ran 78 . . . . . . . . . 10 ((((c v d) v a) ^ (a v b)) ^ b) = ((((c v d) ^ (a v b)) v a) ^ b)
184176, 183tr 62 . . . . . . . . 9 (((c v d) v a) ^ ((a v b) ^ b)) = ((((c v d) ^ (a v b)) v a) ^ b)
185 ancom 74 . . . . . . . . . . . . 13 ((c v d) ^ (a v b)) = ((a v b) ^ (c v d))
186185, 37tr 62 . . . . . . . . . . . 12 ((c v d) ^ (a v b)) = 0
187186ror 71 . . . . . . . . . . 11 (((c v d) ^ (a v b)) v a) = (0 v a)
188 or0r 103 . . . . . . . . . . 11 (0 v a) = a
189187, 188tr 62 . . . . . . . . . 10 (((c v d) ^ (a v b)) v a) = a
190189ran 78 . . . . . . . . 9 ((((c v d) ^ (a v b)) v a) ^ b) = (a ^ b)
191174, 184, 1903tr 65 . . . . . . . 8 (((c v d) v a) ^ b) = (a ^ b)
192191ror 71 . . . . . . 7 ((((c v d) v a) ^ b) v (c v d)) = ((a ^ b) v (c v d))
193168, 169, 1923tr 65 . . . . . 6 (((c v d) v b) ^ ((c v d) v a)) = ((a ^ b) v (c v d))
194 orcom 73 . . . . . 6 ((a ^ b) v (c v d)) = ((c v d) v (a ^ b))
195160, 193, 1943tr 65 . . . . 5 (((b v c) v d) ^ ((a v c) v d)) = ((c v d) v (a ^ b))
196152, 1952an 79 . . . 4 ((((a v b) v d) ^ ((a v b) v c)) ^ (((b v c) v d) ^ ((a v c) v d))) = (((c ^ d) v (a v b)) ^ ((c v d) v (a ^ b)))
197141, 196tr 62 . . 3 ((((a v b) v d) ^ ((b v c) v d)) ^ (((a v b) v c) ^ ((a v c) v d))) = (((c ^ d) v (a v b)) ^ ((c v d) v (a ^ b)))
198 ml 1121 . . . . . . 7 ((c ^ d) v ((a v b) ^ ((c ^ d) v ((c v d) v (a ^ b))))) = (((c ^ d) v (a v b)) ^ ((c ^ d) v ((c v d) v (a ^ b))))
199198cm 61 . . . . . 6 (((c ^ d) v (a v b)) ^ ((c ^ d) v ((c v d) v (a ^ b)))) = ((c ^ d) v ((a v b) ^ ((c ^ d) v ((c v d) v (a ^ b)))))
200 orass 75 . . . . . . . . 9 (((c ^ d) v (c v d)) v (a ^ b)) = ((c ^ d) v ((c v d) v (a ^ b)))
201200cm 61 . . . . . . . 8 ((c ^ d) v ((c v d) v (a ^ b))) = (((c ^ d) v (c v d)) v (a ^ b))
202 leao1 162 . . . . . . . . . 10 (c ^ d) =< (c v d)
203202df-le2 131 . . . . . . . . 9 ((c ^ d) v (c v d)) = (c v d)
204203ror 71 . . . . . . . 8 (((c ^ d) v (c v d)) v (a ^ b)) = ((c v d) v (a ^ b))
205201, 204tr 62 . . . . . . 7 ((c ^ d) v ((c v d) v (a ^ b))) = ((c v d) v (a ^ b))
206205lan 77 . . . . . 6 (((c ^ d) v (a v b)) ^ ((c ^ d) v ((c v d) v (a ^ b)))) = (((c ^ d) v (a v b)) ^ ((c v d) v (a ^ b)))
207205lan 77 . . . . . . 7 ((a v b) ^ ((c ^ d) v ((c v d) v (a ^ b)))) = ((a v b) ^ ((c v d) v (a ^ b)))
208207lor 70 . . . . . 6 ((c ^ d) v ((a v b) ^ ((c ^ d) v ((c v d) v (a ^ b))))) = ((c ^ d) v ((a v b) ^ ((c v d) v (a ^ b))))
209199, 206, 2083tr2 64 . . . . 5 (((c ^ d) v (a v b)) ^ ((c v d) v (a ^ b))) = ((c ^ d) v ((a v b) ^ ((c v d) v (a ^ b))))
210 leao1 162 . . . . . . . . . . 11 (a ^ b) =< (a v b)
211 leid 148 . . . . . . . . . . 11 (a ^ b) =< (a ^ b)
212210, 211ler2an 173 . . . . . . . . . 10 (a ^ b) =< ((a v b) ^ (a ^ b))
213 lear 161 . . . . . . . . . 10 ((a v b) ^ (a ^ b)) =< (a ^ b)
214212, 213lebi 145 . . . . . . . . 9 (a ^ b) = ((a v b) ^ (a ^ b))
215214lor 70 . . . . . . . 8 ((c v d) v (a ^ b)) = ((c v d) v ((a v b) ^ (a ^ b)))
216215lan 77 . . . . . . 7 ((a v b) ^ ((c v d) v (a ^ b))) = ((a v b) ^ ((c v d) v ((a v b) ^ (a ^ b))))
217 mldual 1122 . . . . . . 7 ((a v b) ^ ((c v d) v ((a v b) ^ (a ^ b)))) = (((a v b) ^ (c v d)) v ((a v b) ^ (a ^ b)))
218213, 212lebi 145 . . . . . . . . 9 ((a v b) ^ (a ^ b)) = (a ^ b)
21937, 2182or 72 . . . . . . . 8 (((a v b) ^ (c v d)) v ((a v b) ^ (a ^ b))) = (0 v (a ^ b))
220 or0r 103 . . . . . . . 8 (0 v (a ^ b)) = (a ^ b)
221219, 220tr 62 . . . . . . 7 (((a v b) ^ (c v d)) v ((a v b) ^ (a ^ b))) = (a ^ b)
222216, 217, 2213tr 65 . . . . . 6 ((a v b) ^ ((c v d) v (a ^ b))) = (a ^ b)
223222lor 70 . . . . 5 ((c ^ d) v ((a v b) ^ ((c v d) v (a ^ b)))) = ((c ^ d) v (a ^ b))
224209, 223tr 62 . . . 4 (((c ^ d) v (a v b)) ^ ((c v d) v (a ^ b))) = ((c ^ d) v (a ^ b))
225 orcom 73 . . . 4 ((c ^ d) v (a ^ b)) = ((a ^ b) v (c ^ d))
226224, 225tr 62 . . 3 (((c ^ d) v (a v b)) ^ ((c v d) v (a ^ b))) = ((a ^ b) v (c ^ d))
227140, 197, 2263tr 65 . 2 ((((a v b) v c) ^ ((a v c) v d)) ^ (((a v b) v d) ^ ((b v c) v d))) = ((a ^ b) v (c ^ d))
228139, 227tr 62 1 ((a v c) ^ (b v d)) = ((a ^ b) v (c ^ d))
Colors of variables: term
Syntax hints:   = wb 1   v wo 6   ^ wa 7  0wf 9
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  ax-ml 1120
This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131
  Copyright terms: Public domain W3C validator