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  5229  axprlem4  5373  axprg  5383  dmcosseq  5935  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  fliftfun  7268  tz7.48lem  8382  ssfi  9109  ac6sfi  9196  frfi  9197  domunfican  9234  iunfi  9255  finsschain  9271  cantnfval2  9590  cantnflt  9593  cnfcom  9621  kmlem1  10073  kmlem13  10085  axpowndlem2  10521  wunfi  10644  ingru  10738  xrub  13239  hashf1lem2  14391  caubnd  15294  fsum2d  15706  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  fprod2d  15916  ablfac1eulem  20015  gsumle  20086  mplcoe1  22004  mplcoe5  22007  mdetunilem9  22576  t1t0  23304  fiuncmp  23360  ptcmpfi  23769  isfil2  23812  fsumcn  24829  ovolfiniun  25470  finiunmbl  25513  volfiniun  25516  itgfsum  25796  dvmptfsum  25947  pntrsumbnd  27545  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  nmounbseqi  30864  nmounbseqiALT  30865  isch3  31328  dmdmd  32387  mdslmd1lem2  32413  sumdmdi  32507  dmdbr4ati  32508  dmdbr6ati  32510  gsumvsca1  33319  gsumvsca2  33320  pwsiga  34307  bnj1533  35027  bnj110  35033  bnj1523  35246  dfon2lem8  36001  meran1  36624  mh-setindnd  36686  bj-stabpeirce  36773  bj-bi3ant  36811  bj-ssbid2ALT  36905  bj-spnfw  36912  bj-spst  36931  bj-19.23bit  36933  wl-syls2  37761  heibor1lem  38057  disjimrmoeqec  39056  isltrn2N  40493  cdlemefrs32fva  40773  fiinfi  43926  con3ALT2  44883  alrim3con13v  44886  islinindfis  48806  setrec1lem4  50046