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

Axiom ax-oadist 994
Description: OA Distributive law. In this section, we postulate this temporary axiom (intended not to be used outside of this section) for the OA distributive law, and derive from it the 6-OA, in theorem d6oa 997. This together with the derivation of the distributive law in theorem 4oadist 1044 shows that the OA distributive law is equivalent to the 6-OA. (Contributed by NM, 30-Dec-1998.)
Hypotheses
Ref Expression
oad.1 e = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))
oad.2 f = (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e)
oad.3 h ≤ (a1 d)
oad.4 jf
oad.5 kf
oad.6 (h ∩ (b1 d)) ≤ k
Assertion
Ref Expression
ax-oadist (h ∩ (jk)) = ((hj) ∪ (hk))

Detailed syntax breakdown of Axiom ax-oadist
StepHypRef Expression
1 wvh . . 3 term  h
2 wvj . . . 4 term  j
3 wvk . . . 4 term  k
42, 3wo 6 . . 3 term  (jk)
51, 4wa 7 . 2 term  (h ∩ (jk))
61, 2wa 7 . . 3 term  (hj)
71, 3wa 7 . . 3 term  (hk)
86, 7wo 6 . 2 term  ((hj) ∪ (hk))
95, 8wb 1 1 wff  (h ∩ (jk)) = ((hj) ∪ (hk))
Colors of variables: term
This axiom is referenced by:  d3oa  995  d4oa  996
  Copyright terms: Public domain W3C validator