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

Theorem oa64v 1031
 Description: Derivation of 4-variable OA from 6-variable OA.
Hypotheses
Ref Expression
oa64v.1 ab
oa64v.2 cd
Assertion
Ref Expression
oa64v ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))

Proof of Theorem oa64v
StepHypRef Expression
1 oa64v.1 . . 3 ab
2 oa64v.2 . . 3 cd
3 le0 147 . . 3 0 ≤ 1
41, 2, 3ax-oa6 1030 . 2 (((ab) ∩ (cd)) ∩ (0 ∪ 1)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((a ∪ 0) ∩ (b ∪ 1)) ∪ ((c ∪ 0) ∩ (d ∪ 1)))))))
5 id 59 . 2 0 = 0
6 id 59 . 2 1 = 1
74, 5, 6oa6v4v 933 1 ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))
 Colors of variables: term Syntax hints:   ≤ wle 2  ⊥ wn 4   ∪ 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  ax-oa6 1030 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:  oa63v  1032
 Copyright terms: Public domain W3C validator