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 
|- ( x = y -> ( [ x / y ] ph <-> ph ) )

Proof

Step Hyp Ref Expression
1 sbequ12 
 |-  ( y = x -> ( ph <-> [ x / y ] ph ) )
2 1 bicomd 
 |-  ( y = x -> ( [ x / y ] ph <-> ph ) )
3 2 equcoms 
 |-  ( x = y -> ( [ x / y ] ph <-> ph ) )