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

Axiom ax-4oa 1033
Description: The proper 4-variable OA law.
Assertion
Ref Expression
ax-4oa ((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))) ≤ (b1 d)

Detailed syntax breakdown of Axiom ax-4oa
StepHypRef Expression
1 wva . . . 4 term  a
2 wvd . . . 4 term  d
31, 2wi1 12 . . 3 term  (a1 d)
4 wvb . . . . . 6 term  b
51, 4wa 7 . . . . 5 term  (ab)
64, 2wi1 12 . . . . . 6 term  (b1 d)
73, 6wa 7 . . . . 5 term  ((a1 d) ∩ (b1 d))
85, 7wo 6 . . . 4 term  ((ab) ∪ ((a1 d) ∩ (b1 d)))
9 wvc . . . . . . 7 term  c
101, 9wa 7 . . . . . 6 term  (ac)
119, 2wi1 12 . . . . . . 7 term  (c1 d)
123, 11wa 7 . . . . . 6 term  ((a1 d) ∩ (c1 d))
1310, 12wo 6 . . . . 5 term  ((ac) ∪ ((a1 d) ∩ (c1 d)))
144, 9wa 7 . . . . . 6 term  (bc)
156, 11wa 7 . . . . . 6 term  ((b1 d) ∩ (c1 d))
1614, 15wo 6 . . . . 5 term  ((bc) ∪ ((b1 d) ∩ (c1 d)))
1713, 16wa 7 . . . 4 term  (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))
188, 17wo 6 . . 3 term  (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))
193, 18wa 7 . 2 term  ((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))))
2019, 6wle 2 1 wff  ((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))) ≤ (b1 d)
Colors of variables: term
This axiom is referenced by:  axoa4  1034
  Copyright terms: Public domain W3C validator