Metamath Proof Explorer

Theorem sbequ12

Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993)

Ref Expression
Assertion sbequ12 
|- ( x = y -> ( ph <-> [ y / x ] ph ) )

Proof

Step Hyp Ref Expression
1 sbequ1 
 |-  ( x = y -> ( ph -> [ y / x ] ph ) )
2 sbequ2 
 |-  ( x = y -> ( [ y / x ] ph -> ph ) )
3 1 2 impbid 
 |-  ( x = y -> ( ph <-> [ y / x ] ph ) )