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

Theorem ibir 233
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 192 . 2  |-  ( ph  ->  ( ph  <->  ps )
)
32ibi 232 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  elpr2  3659  eusv2i  4531  ffdm  5403  ov  5967  ovg  5986  oacl  6534  nnacl  6609  elpm2r  6788  cdaxpdom  7815  cdafi  7816  cfcof  7900  hargch  8299  uzaddcl  10275  expcllem  11114  mreunirn  13503  filunirn  17577  pjini  22278  fzspl  23030  bisimp  23121  xrge0tsmsbi  23383  bnj983  28983
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 177
  Copyright terms: Public domain W3C validator