Theorem bj-ax12v3ALT

Description: Alternate proof of bj-ax12v3 . Uses axc11r and axc15 instead of ax-12 . (Contributed by BJ, 6-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-ax12v3ALT	$$⊢x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-5	$$⊢\phi \to \forall y\phi$$
2		axc11r	$$⊢\forall xx=y\to \left(\forall y\phi \to \forall x\phi \right)$$
3		ala1	$$⊢\forall x\phi \to \forall x\left(x=y\to \phi \right)$$
4	1 2 3	syl56	$$⊢\forall xx=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$
5	4	a1d	$$⊢\forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
6		axc15	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
7	5 6	pm2.61i	$$⊢x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$