Theorem imim1i 63

Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Inference associated with imim1 83. Its associated inference is syl 17. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis

Ref	Expression
imim1i.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
imim1i	⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒))

Proof of Theorem imim1i

Step	Hyp	Ref	Expression
1		imim1i.1	. 2 ⊢ (𝜑 → 𝜓)
2		id 22	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	imim12i 62	1 ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  jarr  106  jarl  125  impt  178  pm3.41  493  pm3.42  494  pm2.67-2  890  jaob  960  3jaob  1426  merco1  1715  19.21v  1942  19.39  1988  moimi  2539  r19.30OLD  3121  r19.37  3259  axrep2  5287  dmcosseq  5970  fliftfun  7305  tz7.48lem  8437  ssfi  9169  ac6sfi  9283  frfi  9284  domunfican  9316  iunfi  9336  finsschain  9355  cantnfval2  9660  cantnflt  9663  cnfcom  9691  kmlem1  10141  kmlem13  10153  axpowndlem2  10589  wunfi  10712  ingru  10806  xrub  13287  hashf1lem2  14413  caubnd  15301  fsum2d  15713  fsumabs  15743  fsumrlim  15753  fsumo1  15754  fsumiun  15763  fprod2d  15921  ablfac1eulem  19936  mplcoe1  21583  mplcoe5  21586  mdetunilem9  22113  t1t0  22843  fiuncmp  22899  ptcmpfi  23308  isfil2  23351  fsumcn  24377  ovolfiniun  25009  finiunmbl  25052  volfiniun  25055  itgfsum  25335  dvmptfsum  25483  pntrsumbnd  27058  mulsproplem12  27572  mulsproplem13  27573  mulsproplem14  27574  nmounbseqi  30017  nmounbseqiALT  30018  isch3  30481  dmdmd  31540  mdslmd1lem2  31566  sumdmdi  31660  dmdbr4ati  31661  dmdbr6ati  31663  gsumle  32229  gsumvsca1  32358  gsumvsca2  32359  pwsiga  33116  bnj1533  33851  bnj110  33857  bnj1523  34070  dfon2lem8  34750  meran1  35284  bj-stabpeirce  35418  bj-bi3ant  35455  bj-ssbid2ALT  35528  bj-spnfw  35535  bj-spst  35555  bj-19.23bit  35557  wl-syls2  36366  heibor1lem  36665  isltrn2N  38979  cdlemefrs32fva  39259  fiinfi  42309  con3ALT2  43276  alrim3con13v  43279  islinindfis  47083  setrec1lem4  47688