---

Step * of Lemma implies_transitivity

∀[P,Q,R:ℙ].  ((P ⇒ Q) ⇒ (Q ⇒ R) ⇒ {P ⇒ R})
BY
{ (Unfold `guard` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P,Q,R:\mBbbP{}].    ((P  {}\mRightarrow{}  Q)  {}\mRightarrow{}  (Q  {}\mRightarrow{}  R)  {}\mRightarrow{}  \{P  {}\mRightarrow{}  R\})


By

---

Latex:
(Unfold  `guard`  0  THEN  Auto)

---

Home Index