---

Step * of Lemma bimplies_transitivity

∀[u,v,w:𝔹].  (↑(u ⇒b w)) supposing ((↑(v ⇒b w)) and (↑(u ⇒b v)))
BY
{ (Unfold `bimplies` 0 THEN ((D 0 THENA Auto) THEN AutoBoolCase ⌜u⌝⋅) THEN (D 0 THENA Auto) THEN AutoBoolCase ⌜v⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[u,v,w:\mBbbB{}].    (\muparrow{}(u  {}\mRightarrow{}\msubb{}  w))  supposing  ((\muparrow{}(v  {}\mRightarrow{}\msubb{}  w))  and  (\muparrow{}(u  {}\mRightarrow{}\msubb{}  v)))


By

---

Latex:
(Unfold  `bimplies`  0
  THEN  ((D  0  THENA  Auto)  THEN  AutoBoolCase  \mkleeneopen{}u\mkleeneclose{}\mcdot{})
  THEN  (D  0  THENA  Auto)
  THEN  AutoBoolCase  \mkleeneopen{}v\mkleeneclose{}\mcdot{})

---

Home Index