This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) )