Metamath Proof Explorer

Theorem frege54cor0a

Description: Synonym for logical equivalence. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege54cor0a 
|- ( ( ps <-> ph ) <-> if- ( ps , ph , -. ph ) )

Proof

Step Hyp Ref Expression
1 ax-frege28 
 |-  ( ( ph -> ps ) -> ( -. ps -> -. ph ) )
2 1 anim2i 
 |-  ( ( ( ps -> ph ) /\ ( ph -> ps ) ) -> ( ( ps -> ph ) /\ ( -. ps -> -. ph ) ) )
3 con4 
 |-  ( ( -. ps -> -. ph ) -> ( ph -> ps ) )
4 3 anim2i 
 |-  ( ( ( ps -> ph ) /\ ( -. ps -> -. ph ) ) -> ( ( ps -> ph ) /\ ( ph -> ps ) ) )
5 2 4 impbii 
 |-  ( ( ( ps -> ph ) /\ ( ph -> ps ) ) <-> ( ( ps -> ph ) /\ ( -. ps -> -. ph ) ) )
6 dfbi2 
 |-  ( ( ps <-> ph ) <-> ( ( ps -> ph ) /\ ( ph -> ps ) ) )
7 dfifp2 
 |-  ( if- ( ps , ph , -. ph ) <-> ( ( ps -> ph ) /\ ( -. ps -> -. ph ) ) )
8 5 6 7 3bitr4i 
 |-  ( ( ps <-> ph ) <-> if- ( ps , ph , -. ph ) )