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

Theorem ibir 257
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 213 . 2 (𝜑 → (𝜑𝜓))
32ibi 256 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  elpr2OLD  4337  eusv2i  5004  ffdm  6215  ov  6937  ovg  6956  oacl  7776  nnacl  7852  elpm2r  8033  cdaxpdom  9195  cdafi  9196  cfcof  9280  hargch  9679  uzaddcl  11929  expcllem  13057  lcmfval  15528  lcmf0val  15529  mreunirn  16455  filunirn  21879  ustelimasn  22219  metustfbas  22555  usgreqdrusgr  26666  pjini  28859  fzspl  29851  f1ocnt  29860  xrge0tsmsbi  30087  bnj983  31320  poimirlem16  33730  poimirlem19  33733  poimirlem25  33739  ac6s6  34285  fouriersw  40943  etransclem25  40971  bits0oALTV  42094  uzlidlring  42431  linccl  42705
  Copyright terms: Public domain W3C validator