Theorem sbequ12r

Description: An equality theorem for substitution. (Contributed by NM, 6-Oct-2004) (Proof shortened by Andrew Salmon, 21-Jun-2011)

	Ref	Expression
Assertion	sbequ12r	⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		sbequ12	⊢ ( 𝑦 = 𝑥 → ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜑 ) )
2	1	bicomd	⊢ ( 𝑦 = 𝑥 → ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
3	2	equcoms	⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) )