NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax11i GIF version

Theorem ax11i 1647
Description: Inference that has ax-11 1746 (without y) as its conclusion. Uses only Tarski's FOL axiom schemes. The hypotheses may be eliminable without one or more of these axioms in special cases. Proof similar to Lemma 16 of [Tarski] p. 70. (Contributed by NM, 20-May-2008.)
Hypotheses
Ref Expression
ax11i.1 (x = y → (φψ))
ax11i.2 (ψxψ)
Assertion
Ref Expression
ax11i (x = y → (φx(x = yφ)))

Proof of Theorem ax11i
StepHypRef Expression
1 ax11i.1 . 2 (x = y → (φψ))
2 ax11i.2 . . 3 (ψxψ)
31biimprcd 216 . . 3 (ψ → (x = yφ))
42, 3alrimih 1565 . 2 (ψx(x = yφ))
51, 4syl6bi 219 1 (x = y → (φx(x = yφ)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  ax11wlem  1720
  Copyright terms: Public domain W3C validator