Axiom ax-oa6 1030

Description: Orthoarguesian law (6-variable version). (Contributed by NM, 29-Nov-1998.)

Hypotheses

Ref	Expression
oal6.1	a ≤ b⊥
oal6.2	c ≤ d⊥
oal6.3	e ≤ f⊥

Assertion

Ref	Expression
ax-oa6	(((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))

Detailed syntax breakdown of Axiom ax-oa6

Step	Hyp	Ref	Expression
1		wva	. . . . 5 term  a
2		wvb	. . . . 5 term  b
3	1, 2	wo 6	. . . 4 term  (a ∪ b)
4		wvc	. . . . 5 term  c
5		wvd	. . . . 5 term  d
6	4, 5	wo 6	. . . 4 term  (c ∪ d)
7	3, 6	wa 7	. . 3 term  ((a ∪ b) ∩ (c ∪ d))
8		wve	. . . 4 term  e
9		wvf	. . . 4 term  f
10	8, 9	wo 6	. . 3 term  (e ∪ f)
11	7, 10	wa 7	. 2 term  (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f))
12	1, 4	wo 6	. . . . . . 7 term  (a ∪ c)
13	2, 5	wo 6	. . . . . . 7 term  (b ∪ d)
14	12, 13	wa 7	. . . . . 6 term  ((a ∪ c) ∩ (b ∪ d))
15	1, 8	wo 6	. . . . . . . 8 term  (a ∪ e)
16	2, 9	wo 6	. . . . . . . 8 term  (b ∪ f)
17	15, 16	wa 7	. . . . . . 7 term  ((a ∪ e) ∩ (b ∪ f))
18	4, 8	wo 6	. . . . . . . 8 term  (c ∪ e)
19	5, 9	wo 6	. . . . . . . 8 term  (d ∪ f)
20	18, 19	wa 7	. . . . . . 7 term  ((c ∪ e) ∩ (d ∪ f))
21	17, 20	wo 6	. . . . . 6 term  (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))
22	14, 21	wa 7	. . . . 5 term  (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f))))
23	4, 22	wo 6	. . . 4 term  (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))
24	1, 23	wa 7	. . 3 term  (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f))))))
25	2, 24	wo 6	. 2 term  (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))
26	11, 25	wle 2	1 wff  (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))

This axiom is used by:  oa64v  1031