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

Axiom ax-oal4 1026
 Description: Orthoarguesian law (4-variable version). (Contributed by NM, 1-Dec-1998.)
Hypotheses
Ref Expression
oal4.1 ab
oal4.2 cd
Assertion
Ref Expression
ax-oal4 ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))

Detailed syntax breakdown of Axiom ax-oal4
StepHypRef Expression
1 wva . . . 4 term  a
2 wvb . . . 4 term  b
31, 2wo 6 . . 3 term  (ab)
4 wvc . . . 4 term  c
5 wvd . . . 4 term  d
64, 5wo 6 . . 3 term  (cd)
73, 6wa 7 . 2 term  ((ab) ∩ (cd))
81, 4wo 6 . . . . . 6 term  (ac)
92, 5wo 6 . . . . . 6 term  (bd)
108, 9wa 7 . . . . 5 term  ((ac) ∩ (bd))
114, 10wo 6 . . . 4 term  (c ∪ ((ac) ∩ (bd)))
121, 11wa 7 . . 3 term  (a ∩ (c ∪ ((ac) ∩ (bd))))
132, 12wo 6 . 2 term  (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))
147, 13wle 2 1 wff  ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))
 Colors of variables: term This axiom is referenced by:  oa4cl  1027  oa43v  1028  oa3moa3  1029
 Copyright terms: Public domain W3C validator