Axiom ax-ml 1122

Description: The modular law axiom. (Contributed by NM, 15-Mar-2010.)

Assertion

Ref	Expression
ax-ml	((a ∪ b) ∩ (a ∪ c)) ≤ (a ∪ (b ∩ (a ∪ c)))

Detailed syntax breakdown of Axiom ax-ml

Step	Hyp	Ref	Expression
1		wva	. . . 4 term  a
2		wvb	. . . 4 term  b
3	1, 2	wo 6	. . 3 term  (a ∪ b)
4		wvc	. . . 4 term  c
5	1, 4	wo 6	. . 3 term  (a ∪ c)
6	3, 5	wa 7	. 2 term  ((a ∪ b) ∩ (a ∪ c))
7	2, 5	wa 7	. . 3 term  (b ∩ (a ∪ c))
8	1, 7	wo 6	. 2 term  (a ∪ (b ∩ (a ∪ c)))
9	6, 8	wle 2	1 wff  ((a ∪ b) ∩ (a ∪ c)) ≤ (a ∪ (b ∩ (a ∪ c)))

This axiom is referenced by:  ml  1123