---

Step * 1 1 of Lemma page55


1. [U] : Type
2. [P] : U ⟶ ℙ
3. [Q] : U ⟶ ℙ
4. ∀x:U. (P[x] ⇒ Q[x])@i
⊢ (∀x:U. P[x]) ⇒ (∀x:U. Q[x])
BY
{ (D 0 THENA Auto)⋅ }

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

---

Latex:

---

Latex:

1.  [U]  :  Type
2.  [P]  :  U  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  U  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x:U.  (P[x]  {}\mRightarrow{}  Q[x])@i
\mvdash{}  (\mforall{}x:U.  P[x])  {}\mRightarrow{}  (\mforall{}x:U.  Q[x])


By

---

Latex:
(D  0  THENA  Auto)\mcdot{}

---

Home Index