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  12758  expcllem  13907  lcmfval  16432  lcmf0val  16433  mreunirn  17416  filunirn  23156  ustelimasn  23497  metustfbas  23836  usgreqdrusgr  28315  pjini  30440  fzspl  31488  f1ocnt  31500  xrge0tsmsbi  31695  bnj983  33337  poimirlem16  35990  poimirlem19  35993  poimirlem25  35999  ac6s6  36527  zrtelqelz  40700  fouriersw  44227  etransclem25  44255  ismea  44447  bits0oALTV  45628  uzlidlring  45982  linccl  46250
  Copyright terms: Public domain W3C validator