Metamath Proof Explorer

Theorem bj-ssbid2

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

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

Proof

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