Theorem imim1i 61

Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Inference associated with imim1 81. 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 60	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  104  impt  168  jarl  174  pm2.67-2  416  pm3.41  580  pm3.42  581  jaob  818  3jaob  1382  merco1  1629  19.21v  1855  19.39  1886  r19.37  3067  axrep2  4701  dmcosseq  5308  fliftfun  6462  tz7.48lem  7423  ac6sfi  8089  frfi  8090  domunfican  8118  iunfi  8137  finsschain  8156  cantnfval2  8449  cantnflt  8452  cnfcom  8480  kmlem1  8855  kmlem13  8867  axpowndlem2  9299  wunfi  9422  ingru  9516  xrub  12014  hashf1lem2  13097  caubnd  13946  fsum2d  14344  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  fprod2d  14550  ablfac1eulem  18294  mplcoe1  19286  mplcoe5  19289  mdetunilem9  20245  t1t0  20962  fiuncmp  21017  ptcmpfi  21426  isfil2  21470  fsumcn  22481  ovolfiniun  23076  finiunmbl  23119  volfiniun  23122  itgfsum  23399  dvmptfsum  23542  pntrsumbnd  25055  nbgraf1olem1  25970  nmounbseqi  27016  nmounbseqiALT  27017  isch3  27482  dmdmd  28543  mdslmd1lem2  28569  sumdmdi  28663  dmdbr4ati  28664  dmdbr6ati  28666  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  pwsiga  29520  bnj1533  30176  bnj110  30182  bnj1523  30393  dfon2lem8  30939  meran1  31580  bj-bi3ant  31747  bj-ssbid2ALT  31835  bj-spnfw  31845  bj-spst  31866  bj-19.23bit  31868  bj-axrep2  31977  wl-syls2  32471  heibor1lem  32778  isltrn2N  34424  cdlemefrs32fva  34706  fiinfi  36897  con3ALT2  37757  alrim3con13v  37764  islinindfis  42032  setrec1lem4  42236