Metamath Proof Explorer


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φψ
ax12i.2 ψxψ
Assertion ax12i x=yφxx=yφ

Proof

Step Hyp Ref Expression
1 ax12i.1 x=yφψ
2 ax12i.2 ψxψ
3 1 biimprcd ψx=yφ
4 2 3 alrimih ψxx=yφ
5 1 4 syl6bi x=yφxx=yφ