---

Step * 1 1 of Lemma ancestral-logic-example1

.....assertion..... 
9. ∀x,y:Dom.  ((P x y) ⇒ (Q x y))@i
⊢ ∀x,y:Dom.  ((P x y) ⇒ TC(λa,b.Q a b)(x,y))
BY
{ Repeat (First [FOAllIntro; FOImpliesIntro]) }

1
9. ∀x,y:Dom.  ((P x y) ⇒ (Q x y))@i
10. x : Dom@i
11. y : Dom@i
12. P x y@i
⊢ TC(λa,b.Q a b)(x,y)

---

Latex:


.....assertion..... 
9.  \mforall{}x,y:Dom.    ((P  x  y)  {}\mRightarrow{}  (Q  x  y))@i
\mvdash{}  \mforall{}x,y:Dom.    ((P  x  y)  {}\mRightarrow{}  TC(\mlambda{}a,b.Q  a  b)(x,y))


By

Repeat  (First  [FOAllIntro;  FOImpliesIntro])

---

Home Index