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

Theorem ibir 271
 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 226 . 2 (𝜑 → (𝜑𝜓))
32ibi 270 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  elimh  1080  eusv2i  5263  relsnb  5643  ffdm  6514  ov  7277  ovg  7297  oacl  8147  nnacl  8224  elpm2r  8411  djuxpdom  9600  djufi  9601  cfcof  9689  hargch  10088  uzaddcl  12296  expcllem  13440  lcmfval  15959  lcmf0val  15960  mreunirn  16868  filunirn  22491  ustelimasn  22832  metustfbas  23168  usgreqdrusgr  27362  pjini  29486  fzspl  30543  f1ocnt  30555  xrge0tsmsbi  30747  bnj983  32337  poimirlem16  35072  poimirlem19  35075  poimirlem25  35081  ac6s6  35609  zrtelqelz  39493  fouriersw  42866  etransclem25  42894  ismea  43083  bits0oALTV  44192  uzlidlring  44546  linccl  44816
 Copyright terms: Public domain W3C validator