Metamath Proof Explorer

Theorem bj-ssbid1

Description: A special case of sbequ1 . (Contributed by BJ, 22-Dec-2020)

Ref Expression
Assertion bj-ssbid1 
|- ( ph -> [ x / x ] ph )

Proof

Step Hyp Ref Expression
1 equid 
 |-  x = x
2 sbequ1 
 |-  ( x = x -> ( ph -> [ x / x ] ph ) )
3 1 2 ax-mp 
 |-  ( ph -> [ x / x ] ph )