Metamath Proof Explorer

Theorem sbcid

Description: An identity theorem for substitution. See sbid . (Contributed by Mario Carneiro, 18-Feb-2017)

Ref Expression
Assertion sbcid 
|- ( [. x / x ]. ph <-> ph )

Proof

Step Hyp Ref Expression
1 sbsbc 
 |-  ( [ x / x ] ph <-> [. x / x ]. ph )
2 sbid 
 |-  ( [ x / x ] ph <-> ph )
3 1 2 bitr3i 
 |-  ( [. x / x ]. ph <-> ph )