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  impt  169  jarl  175  pm2.67-2  417  pm3.41  582  pm3.42  583  jaob  822  3jaob  1390  merco1  1638  19.21v  1868  19.39  1899  r19.37  3086  axrep2  4773  dmcosseq  5387  fliftfun  6562  tz7.48lem  7536  ac6sfi  8204  frfi  8205  domunfican  8233  iunfi  8254  finsschain  8273  cantnfval2  8566  cantnflt  8569  cnfcom  8597  kmlem1  8972  kmlem13  8984  axpowndlem2  9420  wunfi  9543  ingru  9637  xrub  12142  hashf1lem2  13240  caubnd  14098  fsum2d  14502  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fsumiun  14553  fprod2d  14711  ablfac1eulem  18471  mplcoe1  19465  mplcoe5  19468  mdetunilem9  20426  t1t0  21152  fiuncmp  21207  ptcmpfi  21616  isfil2  21660  fsumcn  22673  ovolfiniun  23269  finiunmbl  23312  volfiniun  23315  itgfsum  23593  dvmptfsum  23738  pntrsumbnd  25255  nmounbseqi  27632  nmounbseqiALT  27633  isch3  28098  dmdmd  29159  mdslmd1lem2  29185  sumdmdi  29279  dmdbr4ati  29280  dmdbr6ati  29282  gsumle  29779  gsumvsca1  29782  gsumvsca2  29783  pwsiga  30193  bnj1533  30922  bnj110  30928  bnj1523  31139  dfon2lem8  31695  meran1  32410  bj-bi3ant  32574  bj-ssbid2ALT  32646  bj-spnfw  32658  bj-spst  32679  bj-19.23bit  32681  bj-axrep2  32789  wl-syls2  33292  heibor1lem  33608  isltrn2N  35406  cdlemefrs32fva  35688  fiinfi  37878  con3ALT2  38736  alrim3con13v  38743  islinindfis  42238  setrec1lem4  42437