---

Step * 1 1 1 1 of Lemma fo-logic-test1


9. ∀x.(B x) ⇒ (C x)@i
10. x : Dom@i
11. B x@i
12. (B x) ⇒ (C x)@i
⊢ ∃x.C x
BY
{ FOImpliesElim (-1) }

1
9. ∀x.(B x) ⇒ (C x)@i
10. x : Dom@i
11. B x@i
12. (B x) ⇒ (C x)@i
⊢ B x

2
9. ∀x.(B x) ⇒ (C x)@i
10. x : Dom@i
11. B x@i
12. (B x) ⇒ (C x)@i
13. C x@i
⊢ ∃x.C x

---

Latex:

---

Latex:

9.  \mforall{}x.(B  x)  {}\mRightarrow{}  (C  x)@i
10.  x  :  Dom@i
11.  B  x@i
12.  (B  x)  {}\mRightarrow{}  (C  x)@i
\mvdash{}  \mexists{}x.C  x


By

---

Latex:
FOImpliesElim  (-1)

---

Home Index