---

Step * of Lemma bnot_thru_bor

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

---

Latex:

---

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


By

---

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

---

Home Index