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  906  dcbi  939  orbididc  956  trubifal  1436  albiim  1511  hbbi  1572  hbbid  1599  nfbid  1612  spsbbi  1868  sbbi  1988  cleqh  2307  ralbiim  2642  reu8  2976  sseq2  3225  soeq2  4381  fun11  5360  dffo3  5750  isnsg2  13654  bdbi  15961