Theorem wl-axc11r

Description: Same as axc11r , but using ax12 instead of ax-12 directly. This better reflects axiom usage in theorems dependent on it. (Contributed by NM, 25-Jul-2015) Avoid direct use of ax-12 . (Revised by Wolf Lammen, 30-Mar-2024)

	Ref	Expression
Assertion	wl-axc11r	$$⊢\forall yy=x\to \left(\forall x\phi \to \forall y\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ax12	$$⊢y=x\to \left(\forall x\phi \to \forall y\left(y=x\to \phi \right)\right)$$
2	1	sps	$$⊢\forall yy=x\to \left(\forall x\phi \to \forall y\left(y=x\to \phi \right)\right)$$
3		pm2.27	$$⊢y=x\to \left(\left(y=x\to \phi \right)\to \phi \right)$$
4	3	al2imi	$$⊢\forall yy=x\to \left(\forall y\left(y=x\to \phi \right)\to \forall y\phi \right)$$
5	2 4	syld	$$⊢\forall yy=x\to \left(\forall x\phi \to \forall y\phi \right)$$