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

Proof of Theorem dfbi2

Step	Hyp	Ref	Expression
1		dfbi1 192	. 2
2		df-an 371	. 2
3	1, 2	bitr4i 252	1

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

This theorem is referenced by:  dfbi  629  pm4.71  630  pm5.17  888  xor  891  albiim  1699  nfbid  1933  sbbi  2142  cleqhOLD  2573  ralbiim  2989  reu8  3295  sseq2  3525  soeq2  4825  fun11  5658  dffo3  6046  isnsg2  16231  isarchi  27726  axextprim  29073  biimpexp  29093  axextndbi  29237  aibandbiaiffaiffb  32089  aibandbiaiaiffb  32090  bj-cleqh  34358  bj-ifidg  37707  bj-if1bi  37720  bj-ifbibib  37721  bj-ifdfbi  37730  rp-fakeanorass  37737  frege54cor0a  37890

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