---

Step * of Lemma page55

∀[U:Type]. ∀[P,Q:U ⟶ ℙ].  ((∀x:U. (P[x] ⇒ Q[x])) ⇒ (∀x:U. P[x]) ⇒ (∀x:U. Q[x]))
BY
{ RepeatFor 3 ((D 0 THENA Auto)) }

1
1. [U] : Type
2. [P] : U ⟶ ℙ
3. [Q] : U ⟶ ℙ
⊢ (∀x:U. (P[x] ⇒ Q[x])) ⇒ (∀x:U. P[x]) ⇒ (∀x:U. Q[x])

---

Latex:

---

Latex:
\mforall{}[U:Type].  \mforall{}[P,Q:U  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x:U.  (P[x]  {}\mRightarrow{}  Q[x]))  {}\mRightarrow{}  (\mforall{}x:U.  P[x])  {}\mRightarrow{}  (\mforall{}x:U.  Q[x]))


By

---

Latex:
RepeatFor  3  ((D  0  THENA  Auto))

---

Home Index