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	|- ( A. y y = x -> ( A. x ph -> A. y ph ) )

Proof

Step	Hyp	Ref	Expression
1		ax12	|- ( y = x -> ( A. x ph -> A. y ( y = x -> ph ) ) )
2	1	sps	|- ( A. y y = x -> ( A. x ph -> A. y ( y = x -> ph ) ) )
3		pm2.27	|- ( y = x -> ( ( y = x -> ph ) -> ph ) )
4	3	al2imi	|- ( A. y y = x -> ( A. y ( y = x -> ph ) -> A. y ph ) )
5	2 4	syld	|- ( A. y y = x -> ( A. x ph -> A. y ph ) )