Metamath Proof Explorer

Theorem axfrege52a

Description: Justification for ax-frege52a . (Contributed by RP, 17-Apr-2020)

Ref Expression
Assertion axfrege52a 
|- ( ( ph <-> ps ) -> ( if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )

Proof

Step Hyp Ref Expression
1 ifpbi1 
 |-  ( ( ph <-> ps ) -> ( if- ( ph , th , ch ) <-> if- ( ps , th , ch ) ) )
2 1 biimpd 
 |-  ( ( ph <-> ps ) -> ( if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )