MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ibir 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  3801  eusv2i  4687  ffdm  5572  ov  6160  ovg  6179  oacl  6746  nnacl  6821  elpm2r  7001  cdaxpdom  8033  cdafi  8034  cfcof  8118  hargch  8516  uzaddcl  10497  expcllem  11355  mreunirn  13789  filunirn  17875  ustelimasn  18213  metustfbasOLD  18556  metustfbas  18557  pjini  23162  fzspl  24110  xrge0tsmsbi  24185  bnj983  29040
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