Theorem ax12i

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.)

Hypotheses
ax12i.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
ax12i.2
\( \vdash \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash x = y' \rightarrow \varphi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
Proof
l0
ax12i.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
l1
ax12i.2
ax12i.1
biimprcd _
alrimih l1 _
\( \vdash \psi \rightarrow \forall x \, (x = y' \rightarrow \varphi) \)
biimtrdi l0 _