Metamath Proof Explorer

Theorem sbequ12a

Description: An equality theorem for substitution. (Contributed by NM, 2-Jun-1993) (Proof shortened by Wolf Lammen, 23-Jun-2019)

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

Proof

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