Theorem frege54cor0a 38157

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

Assertion

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

Proof of Theorem frege54cor0a

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

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384  if-wif 1012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-frege28 38124

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ifp 1013

This theorem is referenced by:  frege54cor1a  38158  frege55lem1a  38160  frege55lem2a  38161