---

Step * of Lemma page55-again

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

1
1. U : Type@i'
2. P : U ⟶ ℙ@i'
3. Q : U ⟶ ℙ@i'
4. ∀x:U. ((P x) ⇒ (Q x))@i
5. ∀x:U. (P x)@i
6. x : U@i
⊢ 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  6  ((D  0  THENA  Auto))

---

Home Index