QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa8todual Unicode version
Theorem oa8todual 971
Description: Conventional to dual 8-variable OA law.
Hypothesis
Ref Expression
oa8to5.1 (((a' v b') ^ (c' v d')) ^ ((e' v f') ^ (g' v h'))) =< (b' v (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))))
Assertion
Ref Expression
oa8todual (b ^ (a v (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))))))) =< (((a ^ b) v (c ^ d)) v ((e ^ f) v (g ^ h)))
Proof of Theorem oa8todual
StepHypRef Expression
1 oa8to5.1 . . 3 (((a' v b') ^ (c' v d')) ^ ((e' v f') ^ (g' v h'))) =< (b' v (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))))
21lecon 154 . 2 (b' v (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))))' =< (((a' v b') ^ (c' v d')) ^ ((e' v f') ^ (g' v h')))'
3 ax-a1 30 . . . 4 b = b''
4 ax-a1 30 . . . . . 6 a = a''
5 ax-a1 30 . . . . . . . 8 c = c''
6 df-a 40 . . . . . . . . . . . . . 14 (a ^ c) = (a' v c')'
7 df-a 40 . . . . . . . . . . . . . 14 (b ^ d) = (b' v d')'
86, 72or 72 . . . . . . . . . . . . 13 ((a ^ c) v (b ^ d)) = ((a' v c')' v (b' v d')')
9 oran3 93 . . . . . . . . . . . . 13 ((a' v c')' v (b' v d')') = ((a' v c') ^ (b' v d'))'
108, 9ax-r2 36 . . . . . . . . . . . 12 ((a ^ c) v (b ^ d)) = ((a' v c') ^ (b' v d'))'
11 df-a 40 . . . . . . . . . . . . . . . 16 (a ^ g) = (a' v g')'
12 df-a 40 . . . . . . . . . . . . . . . 16 (b ^ h) = (b' v h')'
1311, 122or 72 . . . . . . . . . . . . . . 15 ((a ^ g) v (b ^ h)) = ((a' v g')' v (b' v h')')
14 oran3 93 . . . . . . . . . . . . . . 15 ((a' v g')' v (b' v h')') = ((a' v g') ^ (b' v h'))'
1513, 14ax-r2 36 . . . . . . . . . . . . . 14 ((a ^ g) v (b ^ h)) = ((a' v g') ^ (b' v h'))'
16 df-a 40 . . . . . . . . . . . . . . . 16 (c ^ g) = (c' v g')'
17 df-a 40 . . . . . . . . . . . . . . . 16 (d ^ h) = (d' v h')'
1816, 172or 72 . . . . . . . . . . . . . . 15 ((c ^ g) v (d ^ h)) = ((c' v g')' v (d' v h')')
19 oran3 93 . . . . . . . . . . . . . . 15 ((c' v g')' v (d' v h')') = ((c' v g') ^ (d' v h'))'
2018, 19ax-r2 36 . . . . . . . . . . . . . 14 ((c ^ g) v (d ^ h)) = ((c' v g') ^ (d' v h'))'
2115, 202an 79 . . . . . . . . . . . . 13 (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h))) = (((a' v g') ^ (b' v h'))' ^ ((c' v g') ^ (d' v h'))')
22 anor3 90 . . . . . . . . . . . . 13 (((a' v g') ^ (b' v h'))' ^ ((c' v g') ^ (d' v h'))') = (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))'
2321, 22ax-r2 36 . . . . . . . . . . . 12 (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h))) = (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))'
2410, 232or 72 . . . . . . . . . . 11 (((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) = (((a' v c') ^ (b' v d'))' v (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))')
25 oran3 93 . . . . . . . . . . 11 (((a' v c') ^ (b' v d'))' v (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))') = (((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h'))))'
2624, 25ax-r2 36 . . . . . . . . . 10 (((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) = (((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h'))))'
27 df-a 40 . . . . . . . . . . . . . . . 16 (a ^ e) = (a' v e')'
28 df-a 40 . . . . . . . . . . . . . . . 16 (b ^ f) = (b' v f')'
2927, 282or 72 . . . . . . . . . . . . . . 15 ((a ^ e) v (b ^ f)) = ((a' v e')' v (b' v f')')
30 oran3 93 . . . . . . . . . . . . . . 15 ((a' v e')' v (b' v f')') = ((a' v e') ^ (b' v f'))'
3129, 30ax-r2 36 . . . . . . . . . . . . . 14 ((a ^ e) v (b ^ f)) = ((a' v e') ^ (b' v f'))'
32 df-a 40 . . . . . . . . . . . . . . . . . 18 (e ^ g) = (e' v g')'
33 df-a 40 . . . . . . . . . . . . . . . . . 18 (f ^ h) = (f' v h')'
3432, 332or 72 . . . . . . . . . . . . . . . . 17 ((e ^ g) v (f ^ h)) = ((e' v g')' v (f' v h')')
35 oran3 93 . . . . . . . . . . . . . . . . 17 ((e' v g')' v (f' v h')') = ((e' v g') ^ (f' v h'))'
3634, 35ax-r2 36 . . . . . . . . . . . . . . . 16 ((e ^ g) v (f ^ h)) = ((e' v g') ^ (f' v h'))'
3715, 362an 79 . . . . . . . . . . . . . . 15 (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h))) = (((a' v g') ^ (b' v h'))' ^ ((e' v g') ^ (f' v h'))')
38 anor3 90 . . . . . . . . . . . . . . 15 (((a' v g') ^ (b' v h'))' ^ ((e' v g') ^ (f' v h'))') = (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))'
3937, 38ax-r2 36 . . . . . . . . . . . . . 14 (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h))) = (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))'
4031, 392or 72 . . . . . . . . . . . . 13 (((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) = (((a' v e') ^ (b' v f'))' v (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))')
41 oran3 93 . . . . . . . . . . . . 13 (((a' v e') ^ (b' v f'))' v (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))') = (((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h'))))'
4240, 41ax-r2 36 . . . . . . . . . . . 12 (((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) = (((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h'))))'
43 df-a 40 . . . . . . . . . . . . . . . 16 (c ^ e) = (c' v e')'
44 df-a 40 . . . . . . . . . . . . . . . 16 (d ^ f) = (d' v f')'
4543, 442or 72 . . . . . . . . . . . . . . 15 ((c ^ e) v (d ^ f)) = ((c' v e')' v (d' v f')')
46 oran3 93 . . . . . . . . . . . . . . 15 ((c' v e')' v (d' v f')') = ((c' v e') ^ (d' v f'))'
4745, 46ax-r2 36 . . . . . . . . . . . . . 14 ((c ^ e) v (d ^ f)) = ((c' v e') ^ (d' v f'))'
4820, 362an 79 . . . . . . . . . . . . . . 15 (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))) = (((c' v g') ^ (d' v h'))' ^ ((e' v g') ^ (f' v h'))')
49 anor3 90 . . . . . . . . . . . . . . 15 (((c' v g') ^ (d' v h'))' ^ ((e' v g') ^ (f' v h'))') = (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))'
5048, 49ax-r2 36 . . . . . . . . . . . . . 14 (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))) = (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))'
5147, 502or 72 . . . . . . . . . . . . 13 (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h)))) = (((c' v e') ^ (d' v f'))' v (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))')
52 oran3 93 . . . . . . . . . . . . 13 (((c' v e') ^ (d' v f'))' v (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))') = (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))'
5351, 52ax-r2 36 . . . . . . . . . . . 12 (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h)))) = (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))'
5442, 532an 79 . . . . . . . . . . 11 ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))) = ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h'))))' ^ (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))')
55 anor3 90 . . . . . . . . . . 11 ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h'))))' ^ (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))') = ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))'
5654, 55ax-r2 36 . . . . . . . . . 10 ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))) = ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))'
5726, 562or 72 . . . . . . . . 9 ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h)))))) = ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h'))))' v ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))')
58 oran3 93 . . . . . . . . 9 ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h'))))' v ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))') = ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))))'
5957, 58ax-r2 36 . . . . . . . 8 ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h)))))) = ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))))'
605, 592an 79 . . . . . . 7 (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))))) = (c'' ^ ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))))')
61 anor3 90 . . . . . . 7 (c'' ^ ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))))') = (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))'
6260, 61ax-r2 36 . . . . . 6 (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))))) = (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))'
634, 622or 72 . . . . 5 (a v (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h)))))))) = (a'' v (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))')
64 oran3 93 . . . . 5 (a'' v (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))') = (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))))))'
6563, 64ax-r2 36 . . . 4 (a v (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h)))))))) = (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))))))'
663, 652an 79 . . 3 (b ^ (a v (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))))))) = (b'' ^ (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))))))')
67 anor3 90 . . 3 (b'' ^ (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h'))))))))') = (b' v (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))))'
6866, 67ax-r2 36 . 2 (b ^ (a v (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))))))) = (b' v (a' ^ (c' v ((((a' v c') ^ (b' v d')) ^ (((a' v g') ^ (b' v h')) v ((c' v g') ^ (d' v h')))) ^ ((((a' v e') ^ (b' v f')) ^ (((a' v g') ^ (b' v h')) v ((e' v g') ^ (f' v h')))) v (((c' v e') ^ (d' v f')) ^ (((c' v g') ^ (d' v h')) v ((e' v g') ^ (f' v h')))))))))'
69 df-a 40 . . . . . 6 (a ^ b) = (a' v b')'
70 df-a 40 . . . . . 6 (c ^ d) = (c' v d')'
7169, 702or 72 . . . . 5 ((a ^ b) v (c ^ d)) = ((a' v b')' v (c' v d')')
72 oran3 93 . . . . 5 ((a' v b')' v (c' v d')') = ((a' v b') ^ (c' v d'))'
7371, 72ax-r2 36 . . . 4 ((a ^ b) v (c ^ d)) = ((a' v b') ^ (c' v d'))'
74 df-a 40 . . . . . 6 (e ^ f) = (e' v f')'
75 df-a 40 . . . . . 6 (g ^ h) = (g' v h')'
7674, 752or 72 . . . . 5 ((e ^ f) v (g ^ h)) = ((e' v f')' v (g' v h')')
77 oran3 93 . . . . 5 ((e' v f')' v (g' v h')') = ((e' v f') ^ (g' v h'))'
7876, 77ax-r2 36 . . . 4 ((e ^ f) v (g ^ h)) = ((e' v f') ^ (g' v h'))'
7973, 782or 72 . . 3 (((a ^ b) v (c ^ d)) v ((e ^ f) v (g ^ h))) = (((a' v b') ^ (c' v d'))' v ((e' v f') ^ (g' v h'))')
80 oran3 93 . . 3 (((a' v b') ^ (c' v d'))' v ((e' v f') ^ (g' v h'))') = (((a' v b') ^ (c' v d')) ^ ((e' v f') ^ (g' v h')))'
8179, 80ax-r2 36 . 2 (((a ^ b) v (c ^ d)) v ((e ^ f) v (g ^ h))) = (((a' v b') ^ (c' v d')) ^ ((e' v f') ^ (g' v h')))'
822, 68, 81le3tr1 140 1 (b ^ (a v (c ^ ((((a ^ c) v (b ^ d)) v (((a ^ g) v (b ^ h)) ^ ((c ^ g) v (d ^ h)))) v ((((a ^ e) v (b ^ f)) v (((a ^ g) v (b ^ h)) ^ ((e ^ g) v (f ^ h)))) ^ (((c ^ e) v (d ^ f)) v (((c ^ g) v (d ^ h)) ^ ((e ^ g) v (f ^ h))))))))) =< (((a ^ b) v (c ^ d)) v ((e ^ f) v (g ^ h)))
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   v wo 6   ^ wa 7
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40  df-le1 130  df-le2 131
This theorem is referenced by:  oa8to5  972
  Copyright terms: Public domain W3C validator