QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa6fromdual Unicode version
Theorem oa6fromdual 953
Description: Dual to conventional 6-variable OA law.
Hypothesis
Ref Expression
oa6fromdual.1 (b' ^ (a' v (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f'))))))) =< (((a' ^ b') v (c' ^ d')) v (e' ^ f'))
Assertion
Ref Expression
oa6fromdual (((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
Proof of Theorem oa6fromdual
StepHypRef Expression
1 oa6fromdual.1 . . 3 (b' ^ (a' v (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f'))))))) =< (((a' ^ b') v (c' ^ d')) v (e' ^ f'))
21lecon 154 . 2 (((a' ^ b') v (c' ^ d')) v (e' ^ f'))' =< (b' ^ (a' v (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f')))))))'
3 oran 87 . . . . . 6 (a v b) = (a' ^ b')'
4 oran 87 . . . . . 6 (c v d) = (c' ^ d')'
53, 42an 79 . . . . 5 ((a v b) ^ (c v d)) = ((a' ^ b')' ^ (c' ^ d')')
6 anor3 90 . . . . 5 ((a' ^ b')' ^ (c' ^ d')') = ((a' ^ b') v (c' ^ d'))'
75, 6ax-r2 36 . . . 4 ((a v b) ^ (c v d)) = ((a' ^ b') v (c' ^ d'))'
8 oran 87 . . . 4 (e v f) = (e' ^ f')'
97, 82an 79 . . 3 (((a v b) ^ (c v d)) ^ (e v f)) = (((a' ^ b') v (c' ^ d'))' ^ (e' ^ f')')
10 anor3 90 . . 3 (((a' ^ b') v (c' ^ d'))' ^ (e' ^ f')') = (((a' ^ b') v (c' ^ d')) v (e' ^ f'))'
119, 10ax-r2 36 . 2 (((a v b) ^ (c v d)) ^ (e v f)) = (((a' ^ b') v (c' ^ d')) v (e' ^ f'))'
12 ax-a1 30 . . . 4 b = b''
13 ax-a1 30 . . . . . 6 a = a''
14 ax-a1 30 . . . . . . . 8 c = c''
15 oran 87 . . . . . . . . . . . 12 (a v c) = (a' ^ c')'
16 oran 87 . . . . . . . . . . . 12 (b v d) = (b' ^ d')'
1715, 162an 79 . . . . . . . . . . 11 ((a v c) ^ (b v d)) = ((a' ^ c')' ^ (b' ^ d')')
18 anor3 90 . . . . . . . . . . 11 ((a' ^ c')' ^ (b' ^ d')') = ((a' ^ c') v (b' ^ d'))'
1917, 18ax-r2 36 . . . . . . . . . 10 ((a v c) ^ (b v d)) = ((a' ^ c') v (b' ^ d'))'
20 oran 87 . . . . . . . . . . . . . 14 (a v e) = (a' ^ e')'
21 oran 87 . . . . . . . . . . . . . 14 (b v f) = (b' ^ f')'
2220, 212an 79 . . . . . . . . . . . . 13 ((a v e) ^ (b v f)) = ((a' ^ e')' ^ (b' ^ f')')
23 anor3 90 . . . . . . . . . . . . 13 ((a' ^ e')' ^ (b' ^ f')') = ((a' ^ e') v (b' ^ f'))'
2422, 23ax-r2 36 . . . . . . . . . . . 12 ((a v e) ^ (b v f)) = ((a' ^ e') v (b' ^ f'))'
25 oran 87 . . . . . . . . . . . . . 14 (c v e) = (c' ^ e')'
26 oran 87 . . . . . . . . . . . . . 14 (d v f) = (d' ^ f')'
2725, 262an 79 . . . . . . . . . . . . 13 ((c v e) ^ (d v f)) = ((c' ^ e')' ^ (d' ^ f')')
28 anor3 90 . . . . . . . . . . . . 13 ((c' ^ e')' ^ (d' ^ f')') = ((c' ^ e') v (d' ^ f'))'
2927, 28ax-r2 36 . . . . . . . . . . . 12 ((c v e) ^ (d v f)) = ((c' ^ e') v (d' ^ f'))'
3024, 292or 72 . . . . . . . . . . 11 (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))) = (((a' ^ e') v (b' ^ f'))' v ((c' ^ e') v (d' ^ f'))')
31 oran3 93 . . . . . . . . . . 11 (((a' ^ e') v (b' ^ f'))' v ((c' ^ e') v (d' ^ f'))') = (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f')))'
3230, 31ax-r2 36 . . . . . . . . . 10 (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))) = (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f')))'
3319, 322an 79 . . . . . . . . 9 (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))) = (((a' ^ c') v (b' ^ d'))' ^ (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f')))')
34 anor3 90 . . . . . . . . 9 (((a' ^ c') v (b' ^ d'))' ^ (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f')))') = (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f'))))'
3533, 34ax-r2 36 . . . . . . . 8 (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))) = (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f'))))'
3614, 352or 72 . . . . . . 7 (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))))) = (c'' v (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f'))))')
37 oran3 93 . . . . . . 7 (c'' v (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f'))))') = (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f')))))'
3836, 37ax-r2 36 . . . . . 6 (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))))) = (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f')))))'
3913, 382an 79 . . . . 5 (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))) = (a'' ^ (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f')))))')
40 anor3 90 . . . . 5 (a'' ^ (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f')))))') = (a' v (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f'))))))'
4139, 40ax-r2 36 . . . 4 (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))) = (a' v (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f'))))))'
4212, 412or 72 . . 3 (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))))))) = (b'' v (a' v (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f'))))))')
43 oran3 93 . . 3 (b'' v (a' v (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f'))))))') = (b' ^ (a' v (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f')))))))'
4442, 43ax-r2 36 . 2 (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))))))) = (b' ^ (a' v (c' ^ (((a' ^ c') v (b' ^ d')) v (((a' ^ e') v (b' ^ f')) ^ ((c' ^ e') v (d' ^ f')))))))'
452, 11, 44le3tr1 140 1 (((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
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:  oa6fromdualn  954  oa4to6  965
  Copyright terms: Public domain W3C validator