Metamath Proof Explorer

Theorem frege60b

Description: Swap antecedents of ax-frege58b . Proposition 60 of Frege1879 p. 52. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax-frege58b 
 |-  ( A. x ( ph -> ( ps -> ch ) ) -> [ y / x ] ( ph -> ( ps -> ch ) ) )
2 sbim 
 |-  ( [ y / x ] ( ph -> ( ps -> ch ) ) <-> ( [ y / x ] ph -> [ y / x ] ( ps -> ch ) ) )
3 sbim 
 |-  ( [ y / x ] ( ps -> ch ) <-> ( [ y / x ] ps -> [ y / x ] ch ) )
4 3 imbi2i 
 |-  ( ( [ y / x ] ph -> [ y / x ] ( ps -> ch ) ) <-> ( [ y / x ] ph -> ( [ y / x ] ps -> [ y / x ] ch ) ) )
5 2 4 bitri 
 |-  ( [ y / x ] ( ph -> ( ps -> ch ) ) <-> ( [ y / x ] ph -> ( [ y / x ] ps -> [ y / x ] ch ) ) )
6 1 5 sylib 
 |-  ( A. x ( ph -> ( ps -> ch ) ) -> ( [ y / x ] ph -> ( [ y / x ] ps -> [ y / x ] ch ) ) )
7 frege12 
 |-  ( ( A. x ( ph -> ( ps -> ch ) ) -> ( [ y / x ] ph -> ( [ y / x ] ps -> [ y / x ] ch ) ) ) -> ( A. x ( ph -> ( ps -> ch ) ) -> ( [ y / x ] ps -> ( [ y / x ] ph -> [ y / x ] ch ) ) ) )
8 6 7 ax-mp 
 |-  ( A. x ( ph -> ( ps -> ch ) ) -> ( [ y / x ] ps -> ( [ y / x ] ph -> [ y / x ] ch ) ) )