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  1713  19.21v  1939  19.39  1990  moimi  2538  r19.37  3232  axrep2  5224  axprlem4  5368  dmcosseq  5923  dmcosseqOLD  5924  dmcosseqOLDOLD  5925  fliftfun  7253  tz7.48lem  8370  ssfi  9097  ac6sfi  9189  frfi  9190  domunfican  9230  iunfi  9252  finsschain  9268  cantnfval2  9584  cantnflt  9587  cnfcom  9615  kmlem1  10064  kmlem13  10076  axpowndlem2  10511  wunfi  10634  ingru  10728  xrub  13232  hashf1lem2  14381  caubnd  15284  fsum2d  15696  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  fprod2d  15906  ablfac1eulem  19971  gsumle  20042  mplcoe1  21960  mplcoe5  21963  mdetunilem9  22523  t1t0  23251  fiuncmp  23307  ptcmpfi  23716  isfil2  23759  fsumcn  24777  ovolfiniun  25418  finiunmbl  25461  volfiniun  25464  itgfsum  25744  dvmptfsum  25895  pntrsumbnd  27493  mulsproplem12  28053  mulsproplem13  28054  mulsproplem14  28055  nmounbseqi  30739  nmounbseqiALT  30740  isch3  31203  dmdmd  32262  mdslmd1lem2  32288  sumdmdi  32382  dmdbr4ati  32383  dmdbr6ati  32385  gsumvsca1  33181  gsumvsca2  33182  pwsiga  34099  bnj1533  34821  bnj110  34827  bnj1523  35040  dfon2lem8  35766  meran1  36387  bj-stabpeirce  36530  bj-bi3ant  36565  bj-ssbid2ALT  36639  bj-spnfw  36646  bj-spst  36665  bj-19.23bit  36667  wl-syls2  37485  heibor1lem  37791  isltrn2N  40102  cdlemefrs32fva  40382  fiinfi  43549  con3ALT2  44507  alrim3con13v  44510  islinindfis  48438  setrec1lem4  49679