QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ax-3oa GIF version

Axiom ax-3oa 998
Description: 3-variable consequence of the orthoarguesion law. (Contributed by NM, 20-Jul-1999.)
Assertion
Ref Expression
ax-3oa ((a1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)

Detailed syntax breakdown of Axiom ax-3oa
StepHypRef Expression
1 wva . . . 4 term  a
2 wvc . . . 4 term  c
31, 2wi1 12 . . 3 term  (a1 c)
4 wvb . . . . 5 term  b
51, 4wa 7 . . . 4 term  (ab)
64, 2wi1 12 . . . . 5 term  (b1 c)
73, 6wa 7 . . . 4 term  ((a1 c) ∩ (b1 c))
85, 7wo 6 . . 3 term  ((ab) ∪ ((a1 c) ∩ (b1 c)))
93, 8wa 7 . 2 term  ((a1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c))))
109, 6wle 2 1 wff  ((a1 c) ∩ ((ab) ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)
Colors of variables: term
This axiom is referenced by:  oal2  999  3oa2  1024
  Copyright terms: Public domain W3C validator