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:
Latex:
\mvdash{}  \mforall{}x.(B  x)  {}\mRightarrow{}  (C  x)  {}\mRightarrow{}  \mexists{}z.B  z  {}\mRightarrow{}  \mexists{}y.C  y
By
Latex:
RepeatFor  2  (FOImpliesIntro\mcdot{})
Home
Index