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

Theorem ibir 256
 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 212 . 2 (𝜑 → (𝜑𝜓))
32ibi 255 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195 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 196 This theorem is referenced by:  elpr2OLD  4148  eusv2i  4789  ffdm  5975  ov  6678  ovg  6697  oacl  7502  nnacl  7578  elpm2r  7761  cdaxpdom  8894  cdafi  8895  cfcof  8979  hargch  9374  uzaddcl  11620  expcllem  12733  lcmfval  15172  lcmf0val  15173  mreunirn  16084  filunirn  21496  ustelimasn  21836  metustfbas  22172  pjini  27942  fzspl  28938  f1ocnt  28946  xrge0tsmsbi  29117  bnj983  30275  poimirlem16  32595  poimirlem19  32598  poimirlem25  32604  ac6s6  33150  fouriersw  39124  etransclem25  39152  bits0oALTV  40130  usgreqdrusgr  40768  uzlidlring  41719  linccl  41997
 Copyright terms: Public domain W3C validator