---

Step * of Lemma bnot_thru_band

∀[p,q:Top].  (¬b(p ∧b q) ~ (¬bp) ∨b(¬bq))
BY
{ ((UnivCD THENA Auto) THEN SymbComp 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p,q:Top].    (\mneg{}\msubb{}(p  \mwedge{}\msubb{}  q)  \msim{}  (\mneg{}\msubb{}p)  \mvee{}\msubb{}(\mneg{}\msubb{}q))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  SymbComp  0  THEN  Auto)

---

Home Index