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 223 . 2 (𝜑 → (𝜑𝜓))
32ibi 267 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
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 207
This theorem is referenced by:  elimh  1083  eusv2i  5394  relsnb  5812  ffdm  6765  ov  7577  ovg  7598  oacl  8573  nnacl  8649  elpm2r  8885  djuxpdom  10226  djufi  10227  cfcof  10314  hargch  10713  uzaddcl  12946  expcllem  14113  lcmfval  16658  lcmf0val  16659  mreunirn  17644  filunirn  23890  ustelimasn  24231  metustfbas  24570  zrtelqelz  26801  usgreqdrusgr  29586  pjini  31718  fzspl  32791  f1ocnt  32804  xrge0tsmsbi  33066  bnj983  34965  poimirlem16  37643  poimirlem19  37646  poimirlem25  37652  ac6s6  38179  fouriersw  46246  etransclem25  46274  ismea  46466  bits0oALTV  47668  uzlidlring  48151  linccl  48331  resinsnlem  48771  termc2  49148
  Copyright terms: Public domain W3C validator