Theorem dfbi2 388

Description: A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.)

Assertion

Ref	Expression
dfbi2	|- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )

Proof of Theorem dfbi2

Step	Hyp	Ref	Expression
1		df-bi 117	. . 3 |- ( ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) ) )
2	1	simpli 111	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
3	1	simpri 113	. 2 |- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) )
4	2, 3	impbii 126	1 |- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm4.71  389  pm5.17dc  912  dcbi  945  orbididc  962  ifpdfbidc  994  trubifal  1461  albiim  1536  hbbi  1597  hbbid  1624  nfbid  1637  spsbbi  1893  sbbi  2013  cleqh  2332  ralbiim  2677  reu8  3013  sseq2  3262  soeq2  4437  fun11  5423  dffo3  5824  isnsg2  13920  bdbi  16596