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  4178  eusv2i  4833  ffdm  6029  ov  6745  ovg  6764  oacl  7575  nnacl  7651  elpm2r  7835  cdaxpdom  8971  cdafi  8972  cfcof  9056  hargch  9455  uzaddcl  11704  expcllem  12827  lcmfval  15277  lcmf0val  15278  mreunirn  16201  filunirn  21626  ustelimasn  21966  metustfbas  22302  usgreqdrusgr  26368  pjini  28446  fzspl  29433  f1ocnt  29442  xrge0tsmsbi  29613  bnj983  30782  poimirlem16  33096  poimirlem19  33099  poimirlem25  33105  ac6s6  33651  fouriersw  39785  etransclem25  39813  bits0oALTV  40921  uzlidlring  41247  linccl  41521
 Copyright terms: Public domain W3C validator