Theorem dfbi2 633

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 195	. 2 |- ( ( ph <-> ps ) <-> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) )
2		df-an 373	. 2 |- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) )
3	1, 2	bitr4i 256	1 |- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  dfbi  634  pm4.71  635  pm5.17  897  xor  900  albiim  1744  nfbid  1990  sbbi  2196  cleqhOLD  2539  ralbiim  2961  reu8  3268  sseq2  3487  soeq2  4792  fun11  5664  dffo3  6050  isnsg2  16840  isarchi  28500  axextprim  30330  biimpexp  30350  axextndbi  30452  bj-cleqh  31351  ifpdfbi  36081  ifpidg  36099  ifp1bi  36110  ifpbibib  36118  rp-fakeanorass  36121  frege54cor0a  36361  dffo3f  37344  aibandbiaiffaiffb  38238  aibandbiaiaiffb  38239