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  4052  eusv2i  4650  ffdm  5751  ov  6417  ovg  6436  oacl  7197  nnacl  7272  elpm2r  7448  cdaxpdom  8581  cdafi  8582  cfcof  8666  hargch  9063  uzaddcl  11149  expcllem  12157  mreunirn  14873  filunirn  20251  ustelimasn  20593  metustfbasOLD  20936  metustfbas  20937  pjini  26440  fzspl  27421  xrge0tsmsbi  27601  ac6s6  30508  uzlidlring  32329  linccl  32497  bnj983  33489
  Copyright terms: Public domain W3C validator