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  888  xor  891  albiim  1700  nfbid  1934  sbbi  2143  cleqhOLD  2573  ralbiim  2989  reu8  3295  sseq2  3521  soeq2  4829  fun11  5659  dffo3  6047  isnsg2  16357  isarchi  27878  axextprim  29248  biimpexp  29268  axextndbi  29411  aibandbiaiffaiffb  32250  aibandbiaiaiffb  32251  bj-cleqh  34459  bj-ifidg  37808  bj-if1bi  37821  bj-ifbibib  37822  bj-ifdfbi  37831  rp-fakeanorass  37838  frege54cor0a  37991