Theorem imim1i 64

Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Inference associated with imim1 84. Its associated inference is syl 18. (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 23	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	imim12i 63	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  107  jarl  126  impt  180  pm3.41  497  pm3.42  498  pm2.67-2  904  jaob  976  merco1  1740  19.21v  1966  19.39  2017  r19.37  3274  axrep2  5242  axprlem1  5392  axprlem4  5395  axprg  5406  dmcosseq  5966  dmcosseqOLD  5967  fliftfun  7308  tz7.48lem  8424  ssfi  9153  ac6sfi  9240  frfi  9241  domunfican  9277  iunfi  9296  finsschain  9312  cantnfval2  9634  cantnflt  9637  cnfcom  9665  kmlem1  10130  kmlem13  10142  axpowndlem2  10579  wunfi  10702  ingru  10796  xrub  13334  hashf1lem2  14489  caubnd  15406  fsum2d  15818  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  fprod2d  16031  ablfac1eulem  20140  gsumle  20211  mplcoe1  22153  mplcoe5  22156  mdetunilem9  22742  t1t0  23470  fiuncmp  23526  ptcmpfi  23935  isfil2  23978  fsumcn  24994  ovolfiniun  25625  finiunmbl  25668  volfiniun  25671  itgfsum  25951  dvmptfsum  26099  pntrsumbnd  27692  mulsproplem12  28282  mulsproplem13  28283  mulsproplem14  28284  nmounbseqi  31066  nmounbseqiALT  31067  isch3  31530  dmdmd  32589  mdslmd1lem2  32615  sumdmdi  32709  dmdbr4ati  32710  dmdbr6ati  32712  gsumvsca1  33483  gsumvsca2  33484  pwsiga  34461  bnj1533  35181  bnj110  35187  bnj1523  35400  axpowg2  35479  axpowg3  35480  dfon2lem8  36175  meran1  36807  axtco1from2  36871  dfttc4lem2  36925  mh-setindnd  36933  bj-stabpeirce  37029  bj-bi3ant  37067  bj-ssbid2ALT  37170  bj-spnfw  37178  bj-spst  37199  bj-19.23bit  37201  wl-syls2  38047  heibor1lem  38343  disjimrmoeqec  39342  isltrn2N  40779  cdlemefrs32fva  41059  fiinfi  44184  con3ALT2  45124  alrim3con13v  45127  islinindfis  49107  setrec1lem4  50346