---

Step * 1 1 1 of Lemma ancestral-logic-induction


9. ∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y))@i
⊢ ∀[x,y,z:Dom].  (((B x) ⇒ (B y)) ⇒ ((B y) ⇒ (B z)) ⇒ (B x) ⇒ (B z))
BY
{ RepeatFor 6 ((FOAllIntro ORELSE FOImpliesIntro)) }

1
9. ∀x,y:Dom.  ((R x y) ⇒ (B x) ⇒ (B y))@i
10. [x] : Dom
11. [y] : Dom
12. [z] : Dom
13. (B x) ⇒ (B y)@i
14. (B y) ⇒ (B z)@i
15. B x@i
⊢ B z

---

Latex:



9.  \mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y))@i
\mvdash{}  \mforall{}[x,y,z:Dom].    (((B  x)  {}\mRightarrow{}  (B  y))  {}\mRightarrow{}  ((B  y)  {}\mRightarrow{}  (B  z))  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  z))


By

RepeatFor  6  ((FOAllIntro  ORELSE  FOImpliesIntro))

---

Home Index