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  496  pm3.42  497  pm2.67-2  902  jaob  974  3jaobOLD  1445  merco1  1732  19.21v  1958  19.39  2009  r19.37  3264  axrep2  5227  axprlem1  5377  axprlem4  5380  axprg  5391  dmcosseq  5950  dmcosseqOLD  5951  dmcosseqOLDOLD  5952  fliftfun  7291  tz7.48lem  8406  ssfi  9135  ac6sfi  9222  frfi  9223  domunfican  9260  iunfi  9280  finsschain  9296  cantnfval2  9618  cantnflt  9621  cnfcom  9649  kmlem1  10101  kmlem13  10113  axpowndlem2  10550  wunfi  10673  ingru  10767  xrub  13309  hashf1lem2  14463  caubnd  15377  fsum2d  15789  fsumabs  15820  fsumrlim  15830  fsumo1  15831  fsumiun  15840  fprod2d  16002  ablfac1eulem  20105  gsumle  20176  mplcoe1  22078  mplcoe5  22081  mdetunilem9  22668  t1t0  23396  fiuncmp  23452  ptcmpfi  23861  isfil2  23904  fsumcn  24920  ovolfiniun  25551  finiunmbl  25594  volfiniun  25597  itgfsum  25877  dvmptfsum  26025  pntrsumbnd  27618  mulsproplem12  28208  mulsproplem13  28209  mulsproplem14  28210  nmounbseqi  30937  nmounbseqiALT  30938  isch3  31401  dmdmd  32460  mdslmd1lem2  32486  sumdmdi  32580  dmdbr4ati  32581  dmdbr6ati  32583  gsumvsca1  33367  gsumvsca2  33368  pwsiga  34388  bnj1533  35108  bnj110  35114  bnj1523  35327  axpowg2  35404  axpowg3  35405  dfon2lem8  36099  meran1  36732  axtco1from2  36796  dfttc4lem2  36850  mh-setindnd  36858  bj-stabpeirce  36955  bj-bi3ant  36993  bj-ssbid2ALT  37096  bj-spnfw  37104  bj-spst  37125  bj-19.23bit  37127  wl-syls2  37973  heibor1lem  38269  disjimrmoeqec  39268  isltrn2N  40705  cdlemefrs32fva  40985  fiinfi  44110  con3ALT2  45067  alrim3con13v  45070  islinindfis  49032  setrec1lem4  50272