Metamath Proof Explorer

Theorem frege58bcor

Description: Lemma for frege59b . (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege58bcor 
|- ( A. x ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )

Proof

Step Hyp Ref Expression
1 ax-frege58b 
 |-  ( A. x ( ph -> ps ) -> [ y / x ] ( ph -> ps ) )
2 sbim 
 |-  ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) )
3 1 2 sylib 
 |-  ( A. x ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )