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

Axiom ax-oa6 1030
 Description: Orthoarguesian law (6-variable version).
Hypotheses
Ref Expression
oal6.1 ab
oal6.2 cd
oal6.3 ef
Assertion
Ref Expression
ax-oa6 (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))

Detailed syntax breakdown of Axiom ax-oa6
StepHypRef Expression
1 wva . . . . 5 term  a
2 wvb . . . . 5 term  b
31, 2wo 6 . . . 4 term  (ab)
4 wvc . . . . 5 term  c
5 wvd . . . . 5 term  d
64, 5wo 6 . . . 4 term  (cd)
73, 6wa 7 . . 3 term  ((ab) ∩ (cd))
8 wve . . . 4 term  e
9 wvf . . . 4 term  f
108, 9wo 6 . . 3 term  (ef)
117, 10wa 7 . 2 term  (((ab) ∩ (cd)) ∩ (ef))
121, 4wo 6 . . . . . . 7 term  (ac)
132, 5wo 6 . . . . . . 7 term  (bd)
1412, 13wa 7 . . . . . 6 term  ((ac) ∩ (bd))
151, 8wo 6 . . . . . . . 8 term  (ae)
162, 9wo 6 . . . . . . . 8 term  (bf)
1715, 16wa 7 . . . . . . 7 term  ((ae) ∩ (bf))
184, 8wo 6 . . . . . . . 8 term  (ce)
195, 9wo 6 . . . . . . . 8 term  (df)
2018, 19wa 7 . . . . . . 7 term  ((ce) ∩ (df))
2117, 20wo 6 . . . . . 6 term  (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))
2214, 21wa 7 . . . . 5 term  (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df))))
234, 22wo 6 . . . 4 term  (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))
241, 23wa 7 . . 3 term  (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df))))))
252, 24wo 6 . 2 term  (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))
2611, 25wle 2 1 wff  (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))
 Colors of variables: term This axiom is referenced by:  oa64v  1031
 Copyright terms: Public domain W3C validator