---

Step * 1 1 1 1 1 of Lemma example2


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

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

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

---

Latex:



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


By

FOImpliesElim  (-1)

---

Home Index