Theorem bj-equsal1ti

Description: Inference associated with bj-equsal1t . (Contributed by BJ, 30-Sep-2018)

	Ref	Expression
Hypothesis	bj-equsal1ti.1	⊢ Ⅎ 𝑥 𝜑
Assertion	bj-equsal1ti	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		bj-equsal1ti.1	⊢ Ⅎ 𝑥 𝜑
2		bj-equsal1t	⊢ ( Ⅎ 𝑥 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜑 ) )
3	1 2	ax-mp	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜑 )