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

Theorem ibir 268
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 222 . 2 (𝜑 → (𝜑𝜓))
32ibi 267 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  elimh  1084  eusv2i  5348  relsnb  5755  ffdm  6694  ov  7492  ovg  7512  oacl  8449  nnacl  8526  elpm2r  8717  djuxpdom  10055  djufi  10056  cfcof  10144  hargch  10543  uzaddcl  12759  expcllem  13908  lcmfval  16433  lcmf0val  16434  mreunirn  17417  filunirn  23161  ustelimasn  23502  metustfbas  23841  usgreqdrusgr  28321  pjini  30446  fzspl  31494  f1ocnt  31506  xrge0tsmsbi  31701  bnj983  33343  poimirlem16  36025  poimirlem19  36028  poimirlem25  36034  ac6s6  36562  zrtelqelz  40733  fouriersw  44263  etransclem25  44291  ismea  44483  bits0oALTV  45664  uzlidlring  46018  linccl  46286
  Copyright terms: Public domain W3C validator