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  890  jaob  962  3jaobOLD  1427  merco1  1711  19.21v  1938  19.39  1984  moimi  2548  r19.30OLD  3127  r19.37  3268  axrep2  5306  dmcosseq  5999  dmcosseqOLD  6000  fliftfun  7348  tz7.48lem  8497  ssfi  9240  ac6sfi  9348  frfi  9349  domunfican  9389  iunfi  9411  finsschain  9429  cantnfval2  9738  cantnflt  9741  cnfcom  9769  kmlem1  10220  kmlem13  10232  axpowndlem2  10667  wunfi  10790  ingru  10884  xrub  13374  hashf1lem2  14505  caubnd  15407  fsum2d  15819  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  fprod2d  16029  ablfac1eulem  20116  mplcoe1  22078  mplcoe5  22081  mdetunilem9  22647  t1t0  23377  fiuncmp  23433  ptcmpfi  23842  isfil2  23885  fsumcn  24913  ovolfiniun  25555  finiunmbl  25598  volfiniun  25601  itgfsum  25882  dvmptfsum  26033  pntrsumbnd  27628  mulsproplem12  28171  mulsproplem13  28172  mulsproplem14  28173  nmounbseqi  30809  nmounbseqiALT  30810  isch3  31273  dmdmd  32332  mdslmd1lem2  32358  sumdmdi  32452  dmdbr4ati  32453  dmdbr6ati  32455  gsumle  33074  gsumvsca1  33205  gsumvsca2  33206  pwsiga  34094  bnj1533  34828  bnj110  34834  bnj1523  35047  dfon2lem8  35754  meran1  36377  bj-stabpeirce  36520  bj-bi3ant  36555  bj-ssbid2ALT  36629  bj-spnfw  36636  bj-spst  36655  bj-19.23bit  36657  wl-syls2  37463  heibor1lem  37769  isltrn2N  40077  cdlemefrs32fva  40357  fiinfi  43535  con3ALT2  44501  alrim3con13v  44504  islinindfis  48178  setrec1lem4  48782