QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ax-ml Unicode version
Axiom ax-ml 1120
Description: The modular law axiom.
Assertion
Ref Expression
ax-ml ((a v b) ^ (a v c)) =< (a v (b ^ (a v c)))
Detailed syntax breakdown of Axiom ax-ml
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
51, 4wo 6 . . 3 term (a v c)
63, 5wa 7 . 2 term ((a v b) ^ (a v c))
72, 5wa 7 . . 3 term (b ^ (a v c))
81, 7wo 6 . 2 term (a v (b ^ (a v c)))
96, 8wle 2 1 wff ((a v b) ^ (a v c)) =< (a v (b ^ (a v c)))
Colors of variables: term
This axiom is referenced by:  ml  1121
  Copyright terms: Public domain W3C validator