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	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		ax12	⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) ) )
2	1	sps	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) ) )
3		pm2.27	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 = 𝑥 → 𝜑 ) → 𝜑 ) )
4	3	al2imi	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) → ∀ 𝑦 𝜑 ) )
5	2 4	syld	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜑 ) )