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

Theorem oa6todual 952
 Description: Conventional to dual 6-variable OA law.
Hypothesis
Ref Expression
oa6todual.1 (((ab ) ∩ (cd )) ∩ (ef )) ≤ (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))
Assertion
Ref Expression
oa6todual (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ (((ab) ∪ (cd)) ∪ (ef))

Proof of Theorem oa6todual
StepHypRef Expression
1 oa6todual.1 . . 3 (((ab ) ∩ (cd )) ∩ (ef )) ≤ (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))
21lecon 154 . 2 (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df ))))))) ≤ (((ab ) ∩ (cd )) ∩ (ef ))
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 (ac) = (ac )
7 df-a 40 . . . . . . . . . . . 12 (bd) = (bd )
86, 72or 72 . . . . . . . . . . 11 ((ac) ∪ (bd)) = ((ac ) ∪ (bd ) )
9 oran3 93 . . . . . . . . . . 11 ((ac ) ∪ (bd ) ) = ((ac ) ∩ (bd ))
108, 9ax-r2 36 . . . . . . . . . 10 ((ac) ∪ (bd)) = ((ac ) ∩ (bd ))
11 df-a 40 . . . . . . . . . . . . . 14 (ae) = (ae )
12 df-a 40 . . . . . . . . . . . . . 14 (bf) = (bf )
1311, 122or 72 . . . . . . . . . . . . 13 ((ae) ∪ (bf)) = ((ae ) ∪ (bf ) )
14 oran3 93 . . . . . . . . . . . . 13 ((ae ) ∪ (bf ) ) = ((ae ) ∩ (bf ))
1513, 14ax-r2 36 . . . . . . . . . . . 12 ((ae) ∪ (bf)) = ((ae ) ∩ (bf ))
16 df-a 40 . . . . . . . . . . . . . 14 (ce) = (ce )
17 df-a 40 . . . . . . . . . . . . . 14 (df) = (df )
1816, 172or 72 . . . . . . . . . . . . 13 ((ce) ∪ (df)) = ((ce ) ∪ (df ) )
19 oran3 93 . . . . . . . . . . . . 13 ((ce ) ∪ (df ) ) = ((ce ) ∩ (df ))
2018, 19ax-r2 36 . . . . . . . . . . . 12 ((ce) ∪ (df)) = ((ce ) ∩ (df ))
2115, 202an 79 . . . . . . . . . . 11 (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))) = (((ae ) ∩ (bf )) ∩ ((ce ) ∩ (df )) )
22 anor3 90 . . . . . . . . . . 11 (((ae ) ∩ (bf )) ∩ ((ce ) ∩ (df )) ) = (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))
2321, 22ax-r2 36 . . . . . . . . . 10 (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))) = (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))
2410, 232or 72 . . . . . . . . 9 (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df)))) = (((ac ) ∩ (bd )) ∪ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df ))) )
25 oran3 93 . . . . . . . . 9 (((ac ) ∩ (bd )) ∪ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df ))) ) = (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df ))))
2624, 25ax-r2 36 . . . . . . . 8 (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df)))) = (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df ))))
275, 262an 79 . . . . . . 7 (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))) = (c ∩ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))) )
28 anor3 90 . . . . . . 7 (c ∩ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))) ) = (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))
2927, 28ax-r2 36 . . . . . 6 (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))) = (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))
304, 292or 72 . . . . 5 (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df)))))) = (a ∪ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df ))))) )
31 oran3 93 . . . . 5 (a ∪ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df ))))) ) = (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df ))))))
3230, 31ax-r2 36 . . . 4 (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df)))))) = (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df ))))))
333, 322an 79 . . 3 (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) = (b ∩ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))) )
34 anor3 90 . . 3 (b ∩ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))) ) = (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))
3533, 34ax-r2 36 . 2 (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) = (b ∪ (a ∩ (c ∪ (((ac ) ∩ (bd )) ∩ (((ae ) ∩ (bf )) ∪ ((ce ) ∩ (df )))))))
36 df-a 40 . . . . . 6 (ab) = (ab )
37 df-a 40 . . . . . 6 (cd) = (cd )
3836, 372or 72 . . . . 5 ((ab) ∪ (cd)) = ((ab ) ∪ (cd ) )
39 oran3 93 . . . . 5 ((ab ) ∪ (cd ) ) = ((ab ) ∩ (cd ))
4038, 39ax-r2 36 . . . 4 ((ab) ∪ (cd)) = ((ab ) ∩ (cd ))
41 df-a 40 . . . 4 (ef) = (ef )
4240, 412or 72 . . 3 (((ab) ∪ (cd)) ∪ (ef)) = (((ab ) ∩ (cd )) ∪ (ef ) )
43 oran3 93 . . 3 (((ab ) ∩ (cd )) ∪ (ef ) ) = (((ab ) ∩ (cd )) ∩ (ef ))
4442, 43ax-r2 36 . 2 (((ab) ∪ (cd)) ∪ (ef)) = (((ab ) ∩ (cd )) ∩ (ef ))
452, 35, 44le3tr1 140 1 (b ∩ (a ∪ (c ∩ (((ac) ∪ (bd)) ∪ (((ae) ∪ (bf)) ∩ ((ce) ∪ (df))))))) ≤ (((ab) ∪ (cd)) ∪ (ef))
 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:  oa6to4  958
 Copyright terms: Public domain W3C validator