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  3672  eusv2i  4547  ffdm  5419  ov  5983  ovg  6002  oacl  6550  nnacl  6625  elpm2r  6804  cdaxpdom  7831  cdafi  7832  cfcof  7916  hargch  8315  uzaddcl  10291  expcllem  11130  mreunirn  13519  filunirn  17593  pjini  22294  fzspl  23046  bisimp  23137  xrge0tsmsbi  23398  bnj983  29299
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