Theorem ax12i 1764

Description: Inference that has ax-12 1880 (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
ax12i.1	|- ( x = y -> ( ph <-> ps ) )
ax12i.2	|- ( ps -> A. x ps )

Assertion

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

Proof of Theorem ax12i

Step	Hyp	Ref	Expression
1		ax12i.1	. 2 |- ( x = y -> ( ph <-> ps ) )
2		ax12i.2	. . 3 |- ( ps -> A. x ps )
3	1	biimprcd 227	. . 3 |- ( ps -> ( x = y -> ph ) )
4	2, 3	alrimih 1665	. 2 |- ( ps -> A. x ( x = y -> ph ) )
5	1, 4	syl6bi 230	1 |- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )

Syntax hints:   -> wi 4   <-> wb 186   A.wal 1405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654

This theorem depends on definitions:  df-bi 187

This theorem is referenced by:  ax12wlem  1854