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  492  pm3.42  493  pm2.67-2  891  jaob  963  3jaobOLD  1429  merco1  1714  19.21v  1940  19.39  1991  moimi  2540  r19.37  3235  axrep2  5215  axprlem4  5359  dmcosseq  5912  dmcosseqOLD  5913  dmcosseqOLDOLD  5914  fliftfun  7241  tz7.48lem  8355  ssfi  9077  ac6sfi  9163  frfi  9164  domunfican  9201  iunfi  9222  finsschain  9238  cantnfval2  9554  cantnflt  9557  cnfcom  9585  kmlem1  10037  kmlem13  10049  axpowndlem2  10484  wunfi  10607  ingru  10701  xrub  13206  hashf1lem2  14358  caubnd  15261  fsum2d  15673  fsumabs  15703  fsumrlim  15713  fsumo1  15714  fsumiun  15723  fprod2d  15883  ablfac1eulem  19981  gsumle  20052  mplcoe1  21967  mplcoe5  21970  mdetunilem9  22530  t1t0  23258  fiuncmp  23314  ptcmpfi  23723  isfil2  23766  fsumcn  24783  ovolfiniun  25424  finiunmbl  25467  volfiniun  25470  itgfsum  25750  dvmptfsum  25901  pntrsumbnd  27499  mulsproplem12  28061  mulsproplem13  28062  mulsproplem14  28063  nmounbseqi  30749  nmounbseqiALT  30750  isch3  31213  dmdmd  32272  mdslmd1lem2  32298  sumdmdi  32392  dmdbr4ati  32393  dmdbr6ati  32395  gsumvsca1  33187  gsumvsca2  33188  pwsiga  34135  bnj1533  34856  bnj110  34862  bnj1523  35075  dfon2lem8  35824  meran1  36445  bj-stabpeirce  36588  bj-bi3ant  36623  bj-ssbid2ALT  36697  bj-spnfw  36704  bj-spst  36723  bj-19.23bit  36725  wl-syls2  37543  heibor1lem  37849  isltrn2N  40159  cdlemefrs32fva  40439  fiinfi  43606  con3ALT2  44563  alrim3con13v  44566  islinindfis  48481  setrec1lem4  49722