QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ax-oadist Unicode 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.
Hypotheses
Ref Expression
oad.1 e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))
oad.2 f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)
oad.3 h =< (a ->1 d)
oad.4 j =< f
oad.5 k =< f
oad.6 (h ^ (b ->1 d)) =< k
Assertion
Ref Expression
ax-oadist (h ^ (j v k)) = ((h ^ j) v (h ^ k))
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 (j v k)
51, 4wa 7 . 2 term (h ^ (j v k))
61, 2wa 7 . . 3 term (h ^ j)
71, 3wa 7 . . 3 term (h ^ k)
86, 7wo 6 . 2 term ((h ^ j) v (h ^ k))
95, 8wb 1 1 wff (h ^ (j v k)) = ((h ^ j) v (h ^ k))
Colors of variables: term
This axiom is referenced by:  d3oa  995  d4oa  996
  Copyright terms: Public domain W3C validator