Metamath Proof Explorer

Theorem axfrege52c

Description: Justification for ax-frege52c . (Contributed by RP, 24-Dec-2019)

Ref Expression
Assertion axfrege52c 
|- ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) )

Proof

Step Hyp Ref Expression
1 dfsbcq 
 |-  ( A = B -> ( [. A / x ]. ph <-> [. B / x ]. ph ) )
2 1 biimpd 
 |-  ( A = B -> ( [. A / x ]. ph -> [. B / x ]. ph ) )