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  179  pm3.41  493  pm3.42  494  pm2.67-2  897  jaob  969  3jaobOLD  1435  merco1  1720  19.21v  1946  19.39  1997  r19.37  3242  axrep2  5202  axprlem1  5352  axprlem4  5355  axprg  5366  dmcosseq  5920  dmcosseqOLD  5921  dmcosseqOLDOLD  5922  fliftfun  7256  tz7.48lem  8370  ssfi  9097  ac6sfi  9184  frfi  9185  domunfican  9222  iunfi  9243  finsschain  9259  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  22013  mplcoe5  22016  mdetunilem9  22603  t1t0  23331  fiuncmp  23387  ptcmpfi  23796  isfil2  23839  fsumcn  24855  ovolfiniun  25486  finiunmbl  25529  volfiniun  25532  itgfsum  25812  dvmptfsum  25960  pntrsumbnd  27547  mulsproplem12  28137  mulsproplem13  28138  mulsproplem14  28139  nmounbseqi  30866  nmounbseqiALT  30867  isch3  31330  dmdmd  32389  mdslmd1lem2  32415  sumdmdi  32509  dmdbr4ati  32510  dmdbr6ati  32512  gsumvsca1  33307  gsumvsca2  33308  pwsiga  34314  bnj1533  35034  bnj110  35040  bnj1523  35253  axpowg2  35328  axpowg3  35329  dfon2lem8  36016  meran1  36639  axtco1from2  36703  dfttc4lem2  36757  mh-setindnd  36765  bj-stabpeirce  36862  bj-bi3ant  36900  bj-ssbid2ALT  37003  bj-spnfw  37011  bj-spst  37032  bj-19.23bit  37034  wl-syls2  37880  heibor1lem  38176  disjimrmoeqec  39175  isltrn2N  40612  cdlemefrs32fva  40892  fiinfi  44017  con3ALT2  44974  alrim3con13v  44977  islinindfis  48940  setrec1lem4  50180