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  892  jaob  964  3jaobOLD  1430  merco1  1715  19.21v  1941  19.39  1992  r19.37  3241  axrep2  5215  axprlem1  5360  axprlem4  5363  axprg  5374  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  fliftfun  7260  tz7.48lem  8373  ssfi  9100  ac6sfi  9187  frfi  9188  domunfican  9225  iunfi  9246  finsschain  9262  cantnfval2  9581  cantnflt  9584  cnfcom  9612  kmlem1  10064  kmlem13  10076  axpowndlem2  10512  wunfi  10635  ingru  10729  xrub  13255  hashf1lem2  14409  caubnd  15312  fsum2d  15724  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  fprod2d  15937  ablfac1eulem  20040  gsumle  20111  mplcoe1  22025  mplcoe5  22028  mdetunilem9  22595  t1t0  23323  fiuncmp  23379  ptcmpfi  23788  isfil2  23831  fsumcn  24847  ovolfiniun  25478  finiunmbl  25521  volfiniun  25524  itgfsum  25804  dvmptfsum  25952  pntrsumbnd  27543  mulsproplem12  28133  mulsproplem13  28134  mulsproplem14  28135  nmounbseqi  30863  nmounbseqiALT  30864  isch3  31327  dmdmd  32386  mdslmd1lem2  32412  sumdmdi  32506  dmdbr4ati  32507  dmdbr6ati  32509  gsumvsca1  33302  gsumvsca2  33303  pwsiga  34290  bnj1533  35010  bnj110  35016  bnj1523  35229  dfon2lem8  35986  meran1  36609  axtco1from2  36673  dfttc4lem2  36727  mh-setindnd  36735  bj-stabpeirce  36832  bj-bi3ant  36870  bj-ssbid2ALT  36973  bj-spnfw  36981  bj-spst  37002  bj-19.23bit  37004  wl-syls2  37848  heibor1lem  38144  disjimrmoeqec  39143  isltrn2N  40580  cdlemefrs32fva  40860  fiinfi  44018  con3ALT2  44975  alrim3con13v  44978  islinindfis  48937  setrec1lem4  50177