---

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


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
BY
{ RepeatFor 2 ((FOImpliesElim (-3) THEN Try (FOHyp (-1)))) }

---

Latex:



9.  \mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  (B  x)  {}\mRightarrow{}  (B  y))@i
10.  [x]  :  Dom
11.  [y]  :  Dom
12.  [z]  :  Dom
13.  (B  x)  {}\mRightarrow{}  (B  y)@i
14.  (B  y)  {}\mRightarrow{}  (B  z)@i
15.  B  x@i
\mvdash{}  B  z


By

RepeatFor  2  ((FOImpliesElim  (-3)  THEN  Try  (FOHyp  (-1))))

---

Home Index