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

Theorem ibir 255
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 (𝜑 → (𝜓𝜑))
Assertion
Ref Expression
ibir (𝜑𝜓)

Proof of Theorem ibir
StepHypRef Expression
1 ibir.1 . . 3 (𝜑 → (𝜓𝜑))
21bicomd 211 . 2 (𝜑 → (𝜑𝜓))
32ibi 254 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  elpr2OLD  4144  eusv2i  4781  ffdm  5958  ov  6653  ovg  6672  oacl  7476  nnacl  7552  elpm2r  7735  cdaxpdom  8868  cdafi  8869  cfcof  8953  hargch  9348  uzaddcl  11573  expcllem  12685  lcmfval  15115  lcmf0val  15116  mreunirn  16027  filunirn  21435  ustelimasn  21775  metustfbas  22110  pjini  27745  fzspl  28741  f1ocnt  28749  xrge0tsmsbi  28920  bnj983  30078  poimirlem16  32395  poimirlem19  32398  poimirlem25  32404  ac6s6  32950  fouriersw  38925  etransclem25  38953  bits0oALTV  39932  usgreqdrusgr  40767  uzlidlring  41718  linccl  41996
  Copyright terms: Public domain W3C validator