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  r19.37  3239  axrep2  5227  axprlem4  5371  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  fliftfun  7258  tz7.48lem  8372  ssfi  9097  ac6sfi  9184  frfi  9185  domunfican  9222  iunfi  9243  finsschain  9259  cantnfval2  9578  cantnflt  9581  cnfcom  9609  kmlem1  10061  kmlem13  10073  axpowndlem2  10509  wunfi  10632  ingru  10726  xrub  13227  hashf1lem2  14379  caubnd  15282  fsum2d  15694  fsumabs  15724  fsumrlim  15734  fsumo1  15735  fsumiun  15744  fprod2d  15904  ablfac1eulem  20003  gsumle  20074  mplcoe1  21992  mplcoe5  21995  mdetunilem9  22564  t1t0  23292  fiuncmp  23348  ptcmpfi  23757  isfil2  23800  fsumcn  24817  ovolfiniun  25458  finiunmbl  25501  volfiniun  25504  itgfsum  25784  dvmptfsum  25935  pntrsumbnd  27533  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  nmounbseqi  30852  nmounbseqiALT  30853  isch3  31316  dmdmd  32375  mdslmd1lem2  32401  sumdmdi  32495  dmdbr4ati  32496  dmdbr6ati  32498  gsumvsca1  33308  gsumvsca2  33309  pwsiga  34287  bnj1533  35008  bnj110  35014  bnj1523  35227  dfon2lem8  35982  meran1  36605  mh-setindnd  36667  bj-stabpeirce  36754  bj-bi3ant  36789  bj-ssbid2ALT  36864  bj-spnfw  36871  bj-spst  36890  bj-19.23bit  36892  wl-syls2  37714  heibor1lem  38010  isltrn2N  40380  cdlemefrs32fva  40660  fiinfi  43814  con3ALT2  44771  alrim3con13v  44774  islinindfis  48695  setrec1lem4  49935