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

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

Proof of Theorem oa6fromdualn
StepHypRef Expression
1 oa6fromdualn.1 . . 3 (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ (((ab) ∪ (cd)) ∪ (ef))
2 ax-a1 30 . . . 4 b = b
3 ax-a1 30 . . . . 5 a = a
4 ax-a1 30 . . . . . 6 c = c
53, 42an 79 . . . . . . . 8 (ac) = (a c )
6 ax-a1 30 . . . . . . . . 9 d = d
72, 62an 79 . . . . . . . 8 (bd) = (b d )
85, 72or 72 . . . . . . 7 ((ac) ∪ (bd)) = ((a c ) ∪ (b d ))
9 ax-a1 30 . . . . . . . . . 10 e = e
103, 92an 79 . . . . . . . . 9 (ae) = (a e )
11 ax-a1 30 . . . . . . . . . 10 f = f
122, 112an 79 . . . . . . . . 9 (bf) = (b f )
1310, 122or 72 . . . . . . . 8 ((ae) ∪ (bf)) = ((a e ) ∪ (b f ))
144, 92an 79 . . . . . . . . 9 (ce) = (c e )
156, 112an 79 . . . . . . . . 9 (df) = (d f )
1614, 152or 72 . . . . . . . 8 ((ce) ∪ (df)) = ((c e ) ∪ (d f ))
1713, 162an 79 . . . . . . 7 (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))) = (((a e ) ∪ (b f )) ∩ ((c e ) ∪ (d f )))
188, 172or 72 . . . . . 6 (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df)))) = (((a c ) ∪ (b d )) ∪ (((a e ) ∪ (b f )) ∩ ((c e ) ∪ (d f ))))
194, 182an 79 . . . . 5 (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))) = (c ∩ (((a c ) ∪ (b d )) ∪ (((a e ) ∪ (b f )) ∩ ((c e ) ∪ (d f )))))
203, 192or 72 . . . 4 (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df)))))) = (a ∪ (c ∩ (((a c ) ∪ (b d )) ∪ (((a e ) ∪ (b f )) ∩ ((c e ) ∪ (d f ))))))
212, 202an 79 . . 3 (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) = (b ∩ (a ∪ (c ∩ (((a c ) ∪ (b d )) ∪ (((a e ) ∪ (b f )) ∩ ((c e ) ∪ (d f )))))))
223, 22an 79 . . . . 5 (ab) = (a b )
234, 62an 79 . . . . 5 (cd) = (c d )
2422, 232or 72 . . . 4 ((ab) ∪ (cd)) = ((a b ) ∪ (c d ))
259, 112an 79 . . . 4 (ef) = (e f )
2624, 252or 72 . . 3 (((ab) ∪ (cd)) ∪ (ef)) = (((a b ) ∪ (c d )) ∪ (e f ))
271, 21, 26le3tr2 141 . 2 (b ∩ (a ∪ (c ∩ (((a c ) ∪ (b d )) ∪ (((a e ) ∪ (b f )) ∩ ((c e ) ∪ (d f ))))))) ≤ (((a b ) ∪ (c d )) ∪ (e f ))
2827oa6fromdual 953 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: (None)
  Copyright terms: Public domain W3C validator