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

Theorem oa6fromdual 953
Description: Dual to conventional 6-variable OA law. (Contributed by NM, 22-Dec-1998.)
Hypothesis
Ref Expression
oa6fromdual.1 (b ∩ (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))))))) ≤ (((ab ) ∪ (cd )) ∪ (ef ))
Assertion
Ref Expression
oa6fromdual (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))

Proof of Theorem oa6fromdual
StepHypRef Expression
1 oa6fromdual.1 . . 3 (b ∩ (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))))))) ≤ (((ab ) ∪ (cd )) ∪ (ef ))
21lecon 154 . 2 (((ab ) ∪ (cd )) ∪ (ef )) ≤ (b ∩ (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df )))))))
3 oran 87 . . . . . 6 (ab) = (ab )
4 oran 87 . . . . . 6 (cd) = (cd )
53, 42an 79 . . . . 5 ((ab) ∩ (cd)) = ((ab ) ∩ (cd ) )
6 anor3 90 . . . . 5 ((ab ) ∩ (cd ) ) = ((ab ) ∪ (cd ))
75, 6ax-r2 36 . . . 4 ((ab) ∩ (cd)) = ((ab ) ∪ (cd ))
8 oran 87 . . . 4 (ef) = (ef )
97, 82an 79 . . 3 (((ab) ∩ (cd)) ∩ (ef)) = (((ab ) ∪ (cd )) ∩ (ef ) )
10 anor3 90 . . 3 (((ab ) ∪ (cd )) ∩ (ef ) ) = (((ab ) ∪ (cd )) ∪ (ef ))
119, 10ax-r2 36 . 2 (((ab) ∩ (cd)) ∩ (ef)) = (((ab ) ∪ (cd )) ∪ (ef ))
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 (ac) = (ac )
16 oran 87 . . . . . . . . . . . 12 (bd) = (bd )
1715, 162an 79 . . . . . . . . . . 11 ((ac) ∩ (bd)) = ((ac ) ∩ (bd ) )
18 anor3 90 . . . . . . . . . . 11 ((ac ) ∩ (bd ) ) = ((ac ) ∪ (bd ))
1917, 18ax-r2 36 . . . . . . . . . 10 ((ac) ∩ (bd)) = ((ac ) ∪ (bd ))
20 oran 87 . . . . . . . . . . . . . 14 (ae) = (ae )
21 oran 87 . . . . . . . . . . . . . 14 (bf) = (bf )
2220, 212an 79 . . . . . . . . . . . . 13 ((ae) ∩ (bf)) = ((ae ) ∩ (bf ) )
23 anor3 90 . . . . . . . . . . . . 13 ((ae ) ∩ (bf ) ) = ((ae ) ∪ (bf ))
2422, 23ax-r2 36 . . . . . . . . . . . 12 ((ae) ∩ (bf)) = ((ae ) ∪ (bf ))
25 oran 87 . . . . . . . . . . . . . 14 (ce) = (ce )
26 oran 87 . . . . . . . . . . . . . 14 (df) = (df )
2725, 262an 79 . . . . . . . . . . . . 13 ((ce) ∩ (df)) = ((ce ) ∩ (df ) )
28 anor3 90 . . . . . . . . . . . . 13 ((ce ) ∩ (df ) ) = ((ce ) ∪ (df ))
2927, 28ax-r2 36 . . . . . . . . . . . 12 ((ce) ∩ (df)) = ((ce ) ∪ (df ))
3024, 292or 72 . . . . . . . . . . 11 (((ae) ∩ (bf)) ∪ ((ce) ∩ (df))) = (((ae ) ∪ (bf )) ∪ ((ce ) ∪ (df )) )
31 oran3 93 . . . . . . . . . . 11 (((ae ) ∪ (bf )) ∪ ((ce ) ∪ (df )) ) = (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df )))
3230, 31ax-r2 36 . . . . . . . . . 10 (((ae) ∩ (bf)) ∪ ((ce) ∩ (df))) = (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df )))
3319, 322an 79 . . . . . . . . 9 (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))) = (((ac ) ∪ (bd )) ∩ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))) )
34 anor3 90 . . . . . . . . 9 (((ac ) ∪ (bd )) ∩ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))) ) = (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))))
3533, 34ax-r2 36 . . . . . . . 8 (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))) = (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))))
3614, 352or 72 . . . . . . 7 (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df))))) = (c ∪ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df )))) )
37 oran3 93 . . . . . . 7 (c ∪ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df )))) ) = (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df )))))
3836, 37ax-r2 36 . . . . . 6 (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df))))) = (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df )))))
3913, 382an 79 . . . . 5 (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))) = (a ∩ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))))) )
40 anor3 90 . . . . 5 (a ∩ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))))) ) = (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))))))
4139, 40ax-r2 36 . . . 4 (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))) = (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df ))))))
4212, 412or 72 . . 3 (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df))))))) = (b ∪ (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df )))))) )
43 oran3 93 . . 3 (b ∪ (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df )))))) ) = (b ∩ (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df )))))))
4442, 43ax-r2 36 . 2 (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df))))))) = (b ∩ (a ∪ (c ∩ (((ac ) ∪ (bd )) ∪ (((ae ) ∪ (bf )) ∩ ((ce ) ∪ (df )))))))
452, 11, 44le3tr1 140 1 (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))
Colors of variables: term
Syntax hints:  wle 2   wn 4  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