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

Theorem oa8todual 971
 Description: Conventional to dual 8-variable OA law.
Hypothesis
Ref Expression
oa8to5.1 (((ab ) ∩ (cd )) ∩ ((ef ) ∩ (gh ))) ≤ (b ∪ (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))))
Assertion
Ref Expression
oa8todual (b ∩ (a ∪ (c ∩ ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))))))))) ≤ (((ab) ∪ (cd)) ∪ ((ef) ∪ (gh)))

Proof of Theorem oa8todual
StepHypRef Expression
1 oa8to5.1 . . 3 (((ab ) ∩ (cd )) ∩ ((ef ) ∩ (gh ))) ≤ (b ∪ (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))))
21lecon 154 . 2 (b ∪ (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))))))))) ≤ (((ab ) ∩ (cd )) ∩ ((ef ) ∩ (gh )))
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 . . . . . . . . . . . . . 14 (ac) = (ac )
7 df-a 40 . . . . . . . . . . . . . 14 (bd) = (bd )
86, 72or 72 . . . . . . . . . . . . 13 ((ac) ∪ (bd)) = ((ac ) ∪ (bd ) )
9 oran3 93 . . . . . . . . . . . . 13 ((ac ) ∪ (bd ) ) = ((ac ) ∩ (bd ))
108, 9ax-r2 36 . . . . . . . . . . . 12 ((ac) ∪ (bd)) = ((ac ) ∩ (bd ))
11 df-a 40 . . . . . . . . . . . . . . . 16 (ag) = (ag )
12 df-a 40 . . . . . . . . . . . . . . . 16 (bh) = (bh )
1311, 122or 72 . . . . . . . . . . . . . . 15 ((ag) ∪ (bh)) = ((ag ) ∪ (bh ) )
14 oran3 93 . . . . . . . . . . . . . . 15 ((ag ) ∪ (bh ) ) = ((ag ) ∩ (bh ))
1513, 14ax-r2 36 . . . . . . . . . . . . . 14 ((ag) ∪ (bh)) = ((ag ) ∩ (bh ))
16 df-a 40 . . . . . . . . . . . . . . . 16 (cg) = (cg )
17 df-a 40 . . . . . . . . . . . . . . . 16 (dh) = (dh )
1816, 172or 72 . . . . . . . . . . . . . . 15 ((cg) ∪ (dh)) = ((cg ) ∪ (dh ) )
19 oran3 93 . . . . . . . . . . . . . . 15 ((cg ) ∪ (dh ) ) = ((cg ) ∩ (dh ))
2018, 19ax-r2 36 . . . . . . . . . . . . . 14 ((cg) ∪ (dh)) = ((cg ) ∩ (dh ))
2115, 202an 79 . . . . . . . . . . . . 13 (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh))) = (((ag ) ∩ (bh )) ∩ ((cg ) ∩ (dh )) )
22 anor3 90 . . . . . . . . . . . . 13 (((ag ) ∩ (bh )) ∩ ((cg ) ∩ (dh )) ) = (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))
2321, 22ax-r2 36 . . . . . . . . . . . 12 (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh))) = (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))
2410, 232or 72 . . . . . . . . . . 11 (((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) = (((ac ) ∩ (bd )) ∪ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh ))) )
25 oran3 93 . . . . . . . . . . 11 (((ac ) ∩ (bd )) ∪ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh ))) ) = (((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh ))))
2624, 25ax-r2 36 . . . . . . . . . 10 (((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) = (((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh ))))
27 df-a 40 . . . . . . . . . . . . . . . 16 (ae) = (ae )
28 df-a 40 . . . . . . . . . . . . . . . 16 (bf) = (bf )
2927, 282or 72 . . . . . . . . . . . . . . 15 ((ae) ∪ (bf)) = ((ae ) ∪ (bf ) )
30 oran3 93 . . . . . . . . . . . . . . 15 ((ae ) ∪ (bf ) ) = ((ae ) ∩ (bf ))
3129, 30ax-r2 36 . . . . . . . . . . . . . 14 ((ae) ∪ (bf)) = ((ae ) ∩ (bf ))
32 df-a 40 . . . . . . . . . . . . . . . . . 18 (eg) = (eg )
33 df-a 40 . . . . . . . . . . . . . . . . . 18 (fh) = (fh )
3432, 332or 72 . . . . . . . . . . . . . . . . 17 ((eg) ∪ (fh)) = ((eg ) ∪ (fh ) )
35 oran3 93 . . . . . . . . . . . . . . . . 17 ((eg ) ∪ (fh ) ) = ((eg ) ∩ (fh ))
3634, 35ax-r2 36 . . . . . . . . . . . . . . . 16 ((eg) ∪ (fh)) = ((eg ) ∩ (fh ))
3715, 362an 79 . . . . . . . . . . . . . . 15 (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh))) = (((ag ) ∩ (bh )) ∩ ((eg ) ∩ (fh )) )
38 anor3 90 . . . . . . . . . . . . . . 15 (((ag ) ∩ (bh )) ∩ ((eg ) ∩ (fh )) ) = (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))
3937, 38ax-r2 36 . . . . . . . . . . . . . 14 (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh))) = (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))
4031, 392or 72 . . . . . . . . . . . . 13 (((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) = (((ae ) ∩ (bf )) ∪ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh ))) )
41 oran3 93 . . . . . . . . . . . . 13 (((ae ) ∩ (bf )) ∪ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh ))) ) = (((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh ))))
4240, 41ax-r2 36 . . . . . . . . . . . 12 (((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) = (((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh ))))
43 df-a 40 . . . . . . . . . . . . . . . 16 (ce) = (ce )
44 df-a 40 . . . . . . . . . . . . . . . 16 (df) = (df )
4543, 442or 72 . . . . . . . . . . . . . . 15 ((ce) ∪ (df)) = ((ce ) ∪ (df ) )
46 oran3 93 . . . . . . . . . . . . . . 15 ((ce ) ∪ (df ) ) = ((ce ) ∩ (df ))
4745, 46ax-r2 36 . . . . . . . . . . . . . 14 ((ce) ∪ (df)) = ((ce ) ∩ (df ))
4820, 362an 79 . . . . . . . . . . . . . . 15 (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))) = (((cg ) ∩ (dh )) ∩ ((eg ) ∩ (fh )) )
49 anor3 90 . . . . . . . . . . . . . . 15 (((cg ) ∩ (dh )) ∩ ((eg ) ∩ (fh )) ) = (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))
5048, 49ax-r2 36 . . . . . . . . . . . . . 14 (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))) = (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))
5147, 502or 72 . . . . . . . . . . . . 13 (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh)))) = (((ce ) ∩ (df )) ∪ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))) )
52 oran3 93 . . . . . . . . . . . . 13 (((ce ) ∩ (df )) ∪ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))) ) = (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))))
5351, 52ax-r2 36 . . . . . . . . . . . 12 (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh)))) = (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))))
5442, 532an 79 . . . . . . . . . . 11 ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))))) = ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∩ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))) )
55 anor3 90 . . . . . . . . . . 11 ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∩ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))) ) = ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))
5654, 55ax-r2 36 . . . . . . . . . 10 ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))))) = ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))
5726, 562or 72 . . . . . . . . 9 ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh)))))) = ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∪ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))))) )
58 oran3 93 . . . . . . . . 9 ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∪ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))))) ) = ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))))))
5957, 58ax-r2 36 . . . . . . . 8 ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh)))))) = ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))))))
605, 592an 79 . . . . . . 7 (c ∩ ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))))))) = (c ∩ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))) )
61 anor3 90 . . . . . . 7 (c ∩ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))) ) = (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))
6260, 61ax-r2 36 . . . . . 6 (c ∩ ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))))))) = (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))
634, 622or 72 . . . . 5 (a ∪ (c ∩ ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh)))))))) = (a ∪ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))))))) )
64 oran3 93 . . . . 5 (a ∪ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))))))) ) = (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))))))))
6563, 64ax-r2 36 . . . 4 (a ∪ (c ∩ ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh)))))))) = (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh ))))))))
663, 652an 79 . . 3 (b ∩ (a ∪ (c ∩ ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))))))))) = (b ∩ (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))) )
67 anor3 90 . . 3 (b ∩ (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))) ) = (b ∪ (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))))
6866, 67ax-r2 36 . 2 (b ∩ (a ∪ (c ∩ ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))))))))) = (b ∪ (a ∩ (c ∪ ((((ac ) ∩ (bd )) ∩ (((ag ) ∩ (bh )) ∪ ((cg ) ∩ (dh )))) ∩ ((((ae ) ∩ (bf )) ∩ (((ag ) ∩ (bh )) ∪ ((eg ) ∩ (fh )))) ∪ (((ce ) ∩ (df )) ∩ (((cg ) ∩ (dh )) ∪ ((eg ) ∩ (fh )))))))))
69 df-a 40 . . . . . 6 (ab) = (ab )
70 df-a 40 . . . . . 6 (cd) = (cd )
7169, 702or 72 . . . . 5 ((ab) ∪ (cd)) = ((ab ) ∪ (cd ) )
72 oran3 93 . . . . 5 ((ab ) ∪ (cd ) ) = ((ab ) ∩ (cd ))
7371, 72ax-r2 36 . . . 4 ((ab) ∪ (cd)) = ((ab ) ∩ (cd ))
74 df-a 40 . . . . . 6 (ef) = (ef )
75 df-a 40 . . . . . 6 (gh) = (gh )
7674, 752or 72 . . . . 5 ((ef) ∪ (gh)) = ((ef ) ∪ (gh ) )
77 oran3 93 . . . . 5 ((ef ) ∪ (gh ) ) = ((ef ) ∩ (gh ))
7876, 77ax-r2 36 . . . 4 ((ef) ∪ (gh)) = ((ef ) ∩ (gh ))
7973, 782or 72 . . 3 (((ab) ∪ (cd)) ∪ ((ef) ∪ (gh))) = (((ab ) ∩ (cd )) ∪ ((ef ) ∩ (gh )) )
80 oran3 93 . . 3 (((ab ) ∩ (cd )) ∪ ((ef ) ∩ (gh )) ) = (((ab ) ∩ (cd )) ∩ ((ef ) ∩ (gh )))
8179, 80ax-r2 36 . 2 (((ab) ∪ (cd)) ∪ ((ef) ∪ (gh))) = (((ab ) ∩ (cd )) ∩ ((ef ) ∩ (gh )))
822, 68, 81le3tr1 140 1 (b ∩ (a ∪ (c ∩ ((((ac) ∪ (bd)) ∪ (((ag) ∪ (bh)) ∩ ((cg) ∪ (dh)))) ∪ ((((ae) ∪ (bf)) ∪ (((ag) ∪ (bh)) ∩ ((eg) ∪ (fh)))) ∩ (((ce) ∪ (df)) ∪ (((cg) ∪ (dh)) ∩ ((eg) ∪ (fh))))))))) ≤ (((ab) ∪ (cd)) ∪ ((ef) ∪ (gh)))
 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:  oa8to5  972
 Copyright terms: Public domain W3C validator