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  1082  eusv2i  5393  relsnb  5811  ffdm  6764  ov  7578  ovg  7599  oacl  8574  nnacl  8650  elpm2r  8886  djuxpdom  10227  djufi  10228  cfcof  10315  hargch  10714  uzaddcl  12947  expcllem  14114  lcmfval  16659  lcmf0val  16660  mreunirn  17645  filunirn  23891  ustelimasn  24232  metustfbas  24571  zrtelqelz  26802  usgreqdrusgr  29587  pjini  31719  fzspl  32792  f1ocnt  32805  xrge0tsmsbi  33067  bnj983  34966  poimirlem16  37644  poimirlem19  37647  poimirlem25  37653  ac6s6  38180  fouriersw  46251  etransclem25  46279  ismea  46471  bits0oALTV  47673  uzlidlring  48156  linccl  48336  resinsnlem  48777  termc2  49176  discsntermlem  49222
  Copyright terms: Public domain W3C validator