Theorem dfbi2 628

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

Assertion

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

Proof of Theorem dfbi2

Step	Hyp	Ref	Expression
1		dfbi1 192	. 2 |- ( ( ph <-> ps ) <-> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) )
2		df-an 371	. 2 |- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) )
3	1, 2	bitr4i 252	1 |- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369

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

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  dfbi  629  pm4.71  630  pm5.17  883  xor  886  albiim  1665  nfbid  1866  sbbi  2093  cleqh  2538  ralbiim  2852  reu8  3153  sseq2  3376  soeq2  4659  fun11  5481  dffo3  5856  isnsg2  15709  isarchi  26197  axextprim  27350  biimpexp  27370  axextndbi  27616  aibandbiaiffaiffb  29905  aibandbiaiaiffb  29906  bj-cleqh  32290