Axiom ax-3oa 998

Description: 3-variable consequence of the orthoarguesion law. (Contributed by NM, 20-Jul-1999.)

Assertion

Ref	Expression
ax-3oa	((a →1 c) ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))) ≤ (b →1 c)

Detailed syntax breakdown of Axiom ax-3oa

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

This axiom is used by:  oal2  999  3oa2  1024