QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ax-oal4 Unicode version
Axiom ax-oal4 1026
Description: Orthoarguesian law (4-variable version).
Hypotheses
Ref Expression
oal4.1 a =< b'
oal4.2 c =< d'
Assertion
Ref Expression
ax-oal4 ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
Detailed syntax breakdown of Axiom ax-oal4
StepHypRef Expression
1 wva . . . 4 term a
2 wvb . . . 4 term b
31, 2wo 6 . . 3 term (a v b)
4 wvc . . . 4 term c
5 wvd . . . 4 term d
64, 5wo 6 . . 3 term (c v d)
73, 6wa 7 . 2 term ((a v b) ^ (c v d))
81, 4wo 6 . . . . . 6 term (a v c)
92, 5wo 6 . . . . . 6 term (b v d)
108, 9wa 7 . . . . 5 term ((a v c) ^ (b v d))
114, 10wo 6 . . . 4 term (c v ((a v c) ^ (b v d)))
121, 11wa 7 . . 3 term (a ^ (c v ((a v c) ^ (b v d))))
132, 12wo 6 . 2 term (b v (a ^ (c v ((a v c) ^ (b v d)))))
147, 13wle 2 1 wff ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
Colors of variables: term
This axiom is referenced by:  oa4cl  1027  oa43v  1028  oa3moa3  1029
  Copyright terms: Public domain W3C validator