MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ibir Structured version   Unicode version

Theorem ibir 234
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  |-  ( ph  ->  ( ps  <->  ph ) )
Assertion
Ref Expression
ibir  |-  ( ph  ->  ps )

Proof of Theorem ibir
StepHypRef Expression
1 ibir.1 . . 3  |-  ( ph  ->  ( ps  <->  ph ) )
21bicomd 193 . 2  |-  ( ph  ->  ( ph  <->  ps )
)
32ibi 233 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  elpr2  3833  eusv2i  4720  ffdm  5605  ov  6193  ovg  6212  oacl  6779  nnacl  6854  elpm2r  7034  cdaxpdom  8069  cdafi  8070  cfcof  8154  hargch  8552  uzaddcl  10533  expcllem  11392  mreunirn  13826  filunirn  17914  ustelimasn  18252  metustfbasOLD  18595  metustfbas  18596  pjini  23201  fzspl  24149  xrge0tsmsbi  24224  bnj983  29322
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator