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  3776  eusv2i  4660  ffdm  5545  ov  6132  ovg  6151  oacl  6715  nnacl  6790  elpm2r  6970  cdaxpdom  8002  cdafi  8003  cfcof  8087  hargch  8485  uzaddcl  10465  expcllem  11319  hashf1rn  11563  mreunirn  13753  filunirn  17835  ustelimasn  18173  metustfbas  18477  pjini  23049  fzspl  23985  xrge0tsmsbi  24053  bnj983  28660
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