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

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

Proof of Theorem ibir
StepHypRef Expression
1 ibir.1 . . 3  |-  ( ph  ->  ( ps  <->  ph ) )
21bicomd 201 . 2  |-  ( ph  ->  ( ph  <->  ps )
)
32ibi 241 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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
This theorem is referenced by:  elpr2  4007  eusv2i  4600  ffdm  5683  ov  6323  ovg  6342  oacl  7088  nnacl  7163  elpm2r  7343  cdaxpdom  8473  cdafi  8474  cfcof  8558  hargch  8955  uzaddcl  11026  expcllem  11997  mreunirn  14662  filunirn  19597  ustelimasn  19939  metustfbasOLD  20282  metustfbas  20283  pjini  25281  fzspl  26249  xrge0tsmsbi  26422  ac6s6  29155  linccl  31103  bnj983  32299
  Copyright terms: Public domain W3C validator