Axiom ax-oal4 1026

Description: Orthoarguesian law (4-variable version). (Contributed by NM, 1-Dec-1998.)

Hypotheses

Ref	Expression
oal4.1	a ≤ b⊥
oal4.2	c ≤ d⊥

Assertion

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

Detailed syntax breakdown of Axiom ax-oal4

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		wvd	. . . 4 term  d
6	4, 5	wo 6	. . 3 term  (c ∪ d)
7	3, 6	wa 7	. 2 term  ((a ∪ b) ∩ (c ∪ d))
8	1, 4	wo 6	. . . . . 6 term  (a ∪ c)
9	2, 5	wo 6	. . . . . 6 term  (b ∪ d)
10	8, 9	wa 7	. . . . 5 term  ((a ∪ c) ∩ (b ∪ d))
11	4, 10	wo 6	. . . 4 term  (c ∪ ((a ∪ c) ∩ (b ∪ d)))
12	1, 11	wa 7	. . 3 term  (a ∩ (c ∪ ((a ∪ c) ∩ (b ∪ d))))
13	2, 12	wo 6	. 2 term  (b ∪ (a ∩ (c ∪ ((a ∪ c) ∩ (b ∪ d)))))
14	7, 13	wle 2	1 wff  ((a ∪ b) ∩ (c ∪ d)) ≤ (b ∪ (a ∩ (c ∪ ((a ∪ c) ∩ (b ∪ d)))))

This axiom is used by:  oa4cl  1027  oa43v  1028  oa3moa3  1029