Theorem ax12i

Description: Inference that has ax-12 (without A. y ) as its conclusion. Uses only Tarski's FOL axiom schemes. The hypotheses may be eliminable without using ax-12 in special cases. Proof similar to Lemma 16 of Tarski p. 70. (Contributed by NM, 20-May-2008)

	Ref	Expression
Hypotheses	ax12i.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
	ax12i.2	$$⊢\psi \to \forall x\psi$$
Assertion	ax12i	$$⊢x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax12i.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		ax12i.2	$$⊢\psi \to \forall x\psi$$
3	1	biimprcd	$$⊢\psi \to \left(x=y\to \phi \right)$$
4	2 3	alrimih	$$⊢\psi \to \forall x\left(x=y\to \phi \right)$$
5	1 4	biimtrdi	$$⊢x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$