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  181  pm3.41  496  pm3.42  497  pm2.67-2  892  jaob  962  3jaob  1428  merco1  1721  19.21v  1947  19.39  1993  moimi  2544  r19.30  3253  r19.37  3257  axrep2  5182  dmcosseq  5842  fliftfun  7121  tz7.48lem  8177  ssfi  8851  ac6sfi  8915  frfi  8916  domunfican  8944  iunfi  8964  finsschain  8983  cantnfval2  9284  cantnflt  9287  cnfcom  9315  kmlem1  9764  kmlem13  9776  axpowndlem2  10212  wunfi  10335  ingru  10429  xrub  12902  hashf1lem2  14022  caubnd  14922  fsum2d  15335  fsumabs  15365  fsumrlim  15375  fsumo1  15376  fsumiun  15385  fprod2d  15543  ablfac1eulem  19459  mplcoe1  20994  mplcoe5  20997  mdetunilem9  21517  t1t0  22245  fiuncmp  22301  ptcmpfi  22710  isfil2  22753  fsumcn  23767  ovolfiniun  24398  finiunmbl  24441  volfiniun  24444  itgfsum  24724  dvmptfsum  24872  pntrsumbnd  26447  nmounbseqi  28858  nmounbseqiALT  28859  isch3  29322  dmdmd  30381  mdslmd1lem2  30407  sumdmdi  30501  dmdbr4ati  30502  dmdbr6ati  30504  gsumle  31069  gsumvsca1  31198  gsumvsca2  31199  pwsiga  31810  bnj1533  32545  bnj110  32551  bnj1523  32764  dfon2lem8  33485  meran1  34337  bj-stabpeirce  34471  bj-bi3ant  34508  bj-ssbid2ALT  34581  bj-spnfw  34588  bj-spst  34608  bj-19.23bit  34610  wl-syls2  35405  heibor1lem  35704  isltrn2N  37871  cdlemefrs32fva  38151  fiinfi  40856  con3ALT2  41823  alrim3con13v  41826  islinindfis  45463  setrec1lem4  46067