Theorem dfbi2 385

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 116	. . 3 |- ( ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) ) /\ ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) ) )
2	1	simpli 110	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
3	1	simpri 112	. 2 |- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) )
4	2, 3	impbii 125	1 |- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm4.71  386  pm5.17dc  889  dcbi  920  orbididc  937  trubifal  1394  albiim  1463  hbbi  1527  hbbid  1554  nfbid  1567  spsbbi  1816  sbbi  1930  cleqh  2237  ralbiim  2564  reu8  2875  sseq2  3116  soeq2  4233  fun11  5185  dffo3  5560  bdbi  13013