ax-3oa - Quantum Logic Explorer

Quantum Logic Explorer

< Previous Next >
Related theorems
GIF version

Axiom ax-3oa 998

Description: 3-variable consequence of the orthoarguesion law.

**Assertion**
Ref	Expression
ax-3oa	((a →₁c) ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))) ≤ (b →₁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 →₁c)
4		wvb	. . . . 5 term b
5	1, 4	wa 7	. . . 4 term (a ∩ b)
6	4, 2	wi1 12	. . . . 5 term (b →₁c)
7	3, 6	wa 7	. . . 4 term ((a →₁c) ∩ (b →₁c))
8	5, 7	wo 6	. . 3 term ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))
9	3, 8	wa 7	. 2 term ((a →₁c) ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c))))
10	9, 6	wle 2	1 wff ((a →₁c) ∩ ((a ∩ b) ∪ ((a →₁c) ∩ (b →₁c)))) ≤ (b →₁c)

Colors of variables: term

This axiom is referenced by: oal2 999 3oa2 1024