---

Step * 1 of Lemma example2


⊢ ∀x.(B x) ⇒ (C x) ⇒ ∃z.B z ⇒ ∃y.C y
BY
{ RepeatFor 2 (FOImpliesIntro⋅) }

1
9. ∀x.(B x) ⇒ (C x)@i
10. ∃z.B z@i
⊢ ∃y.C y

---

Latex:



\mvdash{}  \mforall{}x.(B  x)  {}\mRightarrow{}  (C  x)  {}\mRightarrow{}  \mexists{}z.B  z  {}\mRightarrow{}  \mexists{}y.C  y


By

RepeatFor  2  (FOImpliesIntro\mcdot{})

---

Home Index