Theorem dfbi2 626

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 369	. 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 367

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 369

This theorem is referenced by:  dfbi  627  pm4.71  628  pm5.17  887  xor  890  albiim  1718  nfbid  1959  sbbi  2164  cleqhOLD  2516  ralbiim  2936  reu8  3242  sseq2  3461  soeq2  4761  fun11  5588  dffo3  5978  isnsg2  16445  isarchi  28059  axextprim  29778  biimpexp  29798  axextndbi  29905  bj-cleqh  30905  ifpdfbi  35528  ifpidg  35546  ifp1bi  35557  ifpbibib  35565  rp-fakeanorass  35568  frege54cor0a  35808  aibandbiaiffaiffb  37424  aibandbiaiaiffb  37425