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

Theorem oa6v4v 933
Description: 6-variable OA to 4-variable OA. (Contributed by NM, 29-Nov-1998.)
Hypotheses
Ref Expression
oa6v4v.1 (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))
oa6v4v.2 e = 0
oa6v4v.3 f = 1
Assertion
Ref Expression
oa6v4v ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))

Proof of Theorem oa6v4v
StepHypRef Expression
1 oa6v4v.1 . 2 (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))
2 oa6v4v.2 . . . . . 6 e = 0
3 oa6v4v.3 . . . . . 6 f = 1
42, 32or 72 . . . . 5 (ef) = (0 ∪ 1)
5 or0r 103 . . . . 5 (0 ∪ 1) = 1
64, 5ax-r2 36 . . . 4 (ef) = 1
76lan 77 . . 3 (((ab) ∩ (cd)) ∩ (ef)) = (((ab) ∩ (cd)) ∩ 1)
8 an1 106 . . 3 (((ab) ∩ (cd)) ∩ 1) = ((ab) ∩ (cd))
97, 8ax-r2 36 . 2 (((ab) ∩ (cd)) ∩ (ef)) = ((ab) ∩ (cd))
102lor 70 . . . . . . . . . . 11 (ae) = (a ∪ 0)
11 or0 102 . . . . . . . . . . 11 (a ∪ 0) = a
1210, 11ax-r2 36 . . . . . . . . . 10 (ae) = a
133lor 70 . . . . . . . . . . 11 (bf) = (b ∪ 1)
14 or1 104 . . . . . . . . . . 11 (b ∪ 1) = 1
1513, 14ax-r2 36 . . . . . . . . . 10 (bf) = 1
1612, 152an 79 . . . . . . . . 9 ((ae) ∩ (bf)) = (a ∩ 1)
17 an1 106 . . . . . . . . 9 (a ∩ 1) = a
1816, 17ax-r2 36 . . . . . . . 8 ((ae) ∩ (bf)) = a
192lor 70 . . . . . . . . . . 11 (ce) = (c ∪ 0)
20 or0 102 . . . . . . . . . . 11 (c ∪ 0) = c
2119, 20ax-r2 36 . . . . . . . . . 10 (ce) = c
223lor 70 . . . . . . . . . . 11 (df) = (d ∪ 1)
23 or1 104 . . . . . . . . . . 11 (d ∪ 1) = 1
2422, 23ax-r2 36 . . . . . . . . . 10 (df) = 1
2521, 242an 79 . . . . . . . . 9 ((ce) ∩ (df)) = (c ∩ 1)
26 an1 106 . . . . . . . . 9 (c ∩ 1) = c
2725, 26ax-r2 36 . . . . . . . 8 ((ce) ∩ (df)) = c
2818, 272or 72 . . . . . . 7 (((ae) ∩ (bf)) ∪ ((ce) ∩ (df))) = (ac)
2928lan 77 . . . . . 6 (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))) = (((ac) ∩ (bd)) ∩ (ac))
30 an32 83 . . . . . . 7 (((ac) ∩ (bd)) ∩ (ac)) = (((ac) ∩ (ac)) ∩ (bd))
31 anidm 111 . . . . . . . 8 ((ac) ∩ (ac)) = (ac)
3231ran 78 . . . . . . 7 (((ac) ∩ (ac)) ∩ (bd)) = ((ac) ∩ (bd))
3330, 32ax-r2 36 . . . . . 6 (((ac) ∩ (bd)) ∩ (ac)) = ((ac) ∩ (bd))
3429, 33ax-r2 36 . . . . 5 (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))) = ((ac) ∩ (bd))
3534lor 70 . . . 4 (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df))))) = (c ∪ ((ac) ∩ (bd)))
3635lan 77 . . 3 (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))) = (a ∩ (c ∪ ((ac) ∩ (bd))))
3736lor 70 . 2 (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df))))))) = (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))
381, 9, 37le3tr2 141 1 ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))
Colors of variables: term
Syntax hints:   = wb 1  wle 2  wo 6  wa 7  1wt 8  0wf 9
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131
This theorem is referenced by:  oa64v  1031
  Copyright terms: Public domain W3C validator