QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ax-oa6 Unicode version
Axiom ax-oa6 1030
Description: Orthoarguesian law (6-variable version).
Hypotheses
Ref Expression
oal6.1 a =< b'
oal6.2 c =< d'
oal6.3 e =< f'
Assertion
Ref Expression
ax-oa6 (((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
Detailed syntax breakdown of Axiom ax-oa6
StepHypRef Expression
1 wva . . . . 5 term a
2 wvb . . . . 5 term b
31, 2wo 6 . . . 4 term (a v b)
4 wvc . . . . 5 term c
5 wvd . . . . 5 term d
64, 5wo 6 . . . 4 term (c v d)
73, 6wa 7 . . 3 term ((a v b) ^ (c v d))
8 wve . . . 4 term e
9 wvf . . . 4 term f
108, 9wo 6 . . 3 term (e v f)
117, 10wa 7 . 2 term (((a v b) ^ (c v d)) ^ (e v f))
121, 4wo 6 . . . . . . 7 term (a v c)
132, 5wo 6 . . . . . . 7 term (b v d)
1412, 13wa 7 . . . . . 6 term ((a v c) ^ (b v d))
151, 8wo 6 . . . . . . . 8 term (a v e)
162, 9wo 6 . . . . . . . 8 term (b v f)
1715, 16wa 7 . . . . . . 7 term ((a v e) ^ (b v f))
184, 8wo 6 . . . . . . . 8 term (c v e)
195, 9wo 6 . . . . . . . 8 term (d v f)
2018, 19wa 7 . . . . . . 7 term ((c v e) ^ (d v f))
2117, 20wo 6 . . . . . 6 term (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))
2214, 21wa 7 . . . . 5 term (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))))
234, 22wo 6 . . . 4 term (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))
241, 23wa 7 . . 3 term (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f))))))
252, 24wo 6 . 2 term (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
2611, 25wle 2 1 wff (((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))
Colors of variables: term
This axiom is referenced by:  oa64v  1031
  Copyright terms: Public domain W3C validator