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 = (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))))
oad.2	f = (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ 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 ∪ k)) = ((h ∩ j) ∪ (h ∩ k))

Detailed syntax breakdown of Axiom ax-oadist

Step	Hyp	Ref	Expression
1		wvh	. . 3 term  h
2		wvj	. . . 4 term  j
3		wvk	. . . 4 term  k
4	2, 3	wo 6	. . 3 term  (j ∪ k)
5	1, 4	wa 7	. 2 term  (h ∩ (j ∪ k))
6	1, 2	wa 7	. . 3 term  (h ∩ j)
7	1, 3	wa 7	. . 3 term  (h ∩ k)
8	6, 7	wo 6	. 2 term  ((h ∩ j) ∪ (h ∩ k))
9	5, 8	wb 1	1 wff  (h ∩ (j ∪ k)) = ((h ∩ j) ∪ (h ∩ k))

This axiom is used by:  d3oa  995  d4oa  996