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  1426  merco1  1710  19.21v  1937  19.39  1982  moimi  2543  r19.30OLD  3119  r19.37  3260  axrep2  5288  axprlem4  5432  dmcosseq  5990  dmcosseqOLD  5991  fliftfun  7332  tz7.48lem  8480  ssfi  9212  ac6sfi  9318  frfi  9319  domunfican  9359  iunfi  9381  finsschain  9397  cantnfval2  9707  cantnflt  9710  cnfcom  9738  kmlem1  10189  kmlem13  10201  axpowndlem2  10636  wunfi  10759  ingru  10853  xrub  13351  hashf1lem2  14492  caubnd  15394  fsum2d  15804  fsumabs  15834  fsumrlim  15844  fsumo1  15845  fsumiun  15854  fprod2d  16014  ablfac1eulem  20107  mplcoe1  22073  mplcoe5  22076  mdetunilem9  22642  t1t0  23372  fiuncmp  23428  ptcmpfi  23837  isfil2  23880  fsumcn  24908  ovolfiniun  25550  finiunmbl  25593  volfiniun  25596  itgfsum  25877  dvmptfsum  26028  pntrsumbnd  27625  mulsproplem12  28168  mulsproplem13  28169  mulsproplem14  28170  nmounbseqi  30806  nmounbseqiALT  30807  isch3  31270  dmdmd  32329  mdslmd1lem2  32355  sumdmdi  32449  dmdbr4ati  32450  dmdbr6ati  32452  gsumle  33084  gsumvsca1  33215  gsumvsca2  33216  pwsiga  34111  bnj1533  34845  bnj110  34851  bnj1523  35064  dfon2lem8  35772  meran1  36394  bj-stabpeirce  36537  bj-bi3ant  36572  bj-ssbid2ALT  36646  bj-spnfw  36653  bj-spst  36672  bj-19.23bit  36674  wl-syls2  37490  heibor1lem  37796  isltrn2N  40103  cdlemefrs32fva  40383  fiinfi  43563  con3ALT2  44528  alrim3con13v  44531  islinindfis  48295  setrec1lem4  48921