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

Theorem ibir 259
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 214 . 2 (𝜑 → (𝜑𝜓))
32ibi 258 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  eusv2i  5029  ffdm  6244  ov  6978  ovg  6997  oacl  7820  nnacl  7896  elpm2r  8078  cdaxpdom  9264  cdafi  9265  cfcof  9349  hargch  9748  uzaddcl  11944  expcllem  13078  lcmfval  15617  lcmf0val  15618  mreunirn  16529  filunirn  21965  ustelimasn  22305  metustfbas  22641  usgreqdrusgr  26755  pjini  28949  fzspl  29934  f1ocnt  29943  xrge0tsmsbi  30168  bnj983  31401  poimirlem16  33781  poimirlem19  33784  poimirlem25  33790  ac6s6  34333  fouriersw  41017  etransclem25  41045  bits0oALTV  42200  uzlidlring  42530  linccl  42804
  Copyright terms: Public domain W3C validator