Theorem ax11i 1647

Description: Inference that has ax-11 1746 (without A.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 -> (ph <-> ps))
ax11i.2	|- (ps -> A.xps)

Assertion

Ref	Expression
ax11i	|- (x = y -> (ph -> A.x(x = y -> ph)))

Proof of Theorem ax11i

Step	Hyp	Ref	Expression
1		ax11i.1	. 2 |- (x = y -> (ph <-> ps))
2		ax11i.2	. . 3 |- (ps -> A.xps)
3	1	biimprcd 216	. . 3 |- (ps -> (x = y -> ph))
4	2, 3	alrimih 1565	. 2 |- (ps -> A.x(x = y -> ph))
5	1, 4	syl6bi 219	1 |- (x = y -> (ph -> A.x(x = y -> ph)))

Syntax hints:   -> wi 4   <-> wb 176  A.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