QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa6todual Unicode version
Theorem oa6todual 952
Description: Conventional to dual 6-variable OA law.
Hypothesis
Ref Expression
oa6todual.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')))))))
Assertion
Ref Expression
oa6todual (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))
Proof of Theorem oa6todual
StepHypRef Expression
1 oa6todual.1 . . 3 (((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')))))))
21lecon 154 . 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')))))))' =< (((a' v b') ^ (c' v d')) ^ (e' v f'))'
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 . . . . . . . . . . . 12 (a ^ c) = (a' v c')'
7 df-a 40 . . . . . . . . . . . 12 (b ^ d) = (b' v d')'
86, 72or 72 . . . . . . . . . . 11 ((a ^ c) v (b ^ d)) = ((a' v c')' v (b' v d')')
9 oran3 93 . . . . . . . . . . 11 ((a' v c')' v (b' v d')') = ((a' v c') ^ (b' v d'))'
108, 9ax-r2 36 . . . . . . . . . 10 ((a ^ c) v (b ^ d)) = ((a' v c') ^ (b' v d'))'
11 df-a 40 . . . . . . . . . . . . . 14 (a ^ e) = (a' v e')'
12 df-a 40 . . . . . . . . . . . . . 14 (b ^ f) = (b' v f')'
1311, 122or 72 . . . . . . . . . . . . 13 ((a ^ e) v (b ^ f)) = ((a' v e')' v (b' v f')')
14 oran3 93 . . . . . . . . . . . . 13 ((a' v e')' v (b' v f')') = ((a' v e') ^ (b' v f'))'
1513, 14ax-r2 36 . . . . . . . . . . . 12 ((a ^ e) v (b ^ f)) = ((a' v e') ^ (b' v f'))'
16 df-a 40 . . . . . . . . . . . . . 14 (c ^ e) = (c' v e')'
17 df-a 40 . . . . . . . . . . . . . 14 (d ^ f) = (d' v f')'
1816, 172or 72 . . . . . . . . . . . . 13 ((c ^ e) v (d ^ f)) = ((c' v e')' v (d' v f')')
19 oran3 93 . . . . . . . . . . . . 13 ((c' v e')' v (d' v f')') = ((c' v e') ^ (d' v f'))'
2018, 19ax-r2 36 . . . . . . . . . . . 12 ((c ^ e) v (d ^ f)) = ((c' v e') ^ (d' v f'))'
2115, 202an 79 . . . . . . . . . . 11 (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f))) = (((a' v e') ^ (b' v f'))' ^ ((c' v e') ^ (d' v f'))')
22 anor3 90 . . . . . . . . . . 11 (((a' v e') ^ (b' v f'))' ^ ((c' v e') ^ (d' v f'))') = (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f')))'
2321, 22ax-r2 36 . . . . . . . . . 10 (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f))) = (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f')))'
2410, 232or 72 . . . . . . . . 9 (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f)))) = (((a' v c') ^ (b' v d'))' v (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f')))')
25 oran3 93 . . . . . . . . 9 (((a' v c') ^ (b' v d'))' v (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f')))') = (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f'))))'
2624, 25ax-r2 36 . . . . . . . 8 (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f)))) = (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f'))))'
275, 262an 79 . . . . . . 7 (c ^ (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f))))) = (c'' ^ (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f'))))')
28 anor3 90 . . . . . . 7 (c'' ^ (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f'))))') = (c' v (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f')))))'
2927, 28ax-r2 36 . . . . . 6 (c ^ (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f))))) = (c' v (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f')))))'
304, 292or 72 . . . . 5 (a v (c ^ (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f)))))) = (a'' v (c' v (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f')))))')
31 oran3 93 . . . . 5 (a'' v (c' v (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f')))))') = (a' ^ (c' v (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f'))))))'
3230, 31ax-r2 36 . . . 4 (a v (c ^ (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f)))))) = (a' ^ (c' v (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f'))))))'
333, 322an 79 . . 3 (b ^ (a v (c ^ (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ f))))))) = (b'' ^ (a' ^ (c' v (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f'))))))')
34 anor3 90 . . 3 (b'' ^ (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' ^ (c' v (((a' v c') ^ (b' v d')) ^ (((a' v e') ^ (b' v f')) v ((c' v e') ^ (d' v f')))))))'
3533, 34ax-r2 36 . 2 (b ^ (a v (c ^ (((a ^ c) v (b ^ d)) v (((a ^ e) v (b ^ f)) ^ ((c ^ e) v (d ^ 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')))))))'
36 df-a 40 . . . . . 6 (a ^ b) = (a' v b')'
37 df-a 40 . . . . . 6 (c ^ d) = (c' v d')'
3836, 372or 72 . . . . 5 ((a ^ b) v (c ^ d)) = ((a' v b')' v (c' v d')')
39 oran3 93 . . . . 5 ((a' v b')' v (c' v d')') = ((a' v b') ^ (c' v d'))'
4038, 39ax-r2 36 . . . 4 ((a ^ b) v (c ^ d)) = ((a' v b') ^ (c' v d'))'
41 df-a 40 . . . 4 (e ^ f) = (e' v f')'
4240, 412or 72 . . 3 (((a ^ b) v (c ^ d)) v (e ^ f)) = (((a' v b') ^ (c' v d'))' v (e' v f')')
43 oran3 93 . . 3 (((a' v b') ^ (c' v d'))' v (e' v f')') = (((a' v b') ^ (c' v d')) ^ (e' v f'))'
4442, 43ax-r2 36 . 2 (((a ^ b) v (c ^ d)) v (e ^ f)) = (((a' v b') ^ (c' v d')) ^ (e' v f'))'
452, 35, 44le3tr1 140 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))
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:  oa6to4  958
  Copyright terms: Public domain W3C validator