Theorem ibir 242

Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.)

Hypothesis

Ref	Expression
ibir.1

Assertion

Ref	Expression
ibir

Proof of Theorem ibir

Step	Hyp	Ref	Expression
1		ibir.1	. . 3
2	1	bicomd 201	. 2
3	2	ibi 241	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  elpr2  4048  eusv2i  4649  ffdm  5750  ov  6422  ovg  6441  oacl  7204  nnacl  7279  elpm2r  7456  cdaxpdom  8590  cdafi  8591  cfcof  8675  hargch  9072  uzaddcl  11166  expcllem  12177  mreunirn  14998  filunirn  20383  ustelimasn  20725  metustfbasOLD  21068  metustfbas  21069  pjini  26617  fzspl  27598  xrge0tsmsbi  27776  ac6s6  30580  fouriersw  32014  etransclem25  32042  uzlidlring  32735  linccl  33015  bnj983  34009

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