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  494  pm3.42  495  pm2.67-2  891  jaob  961  3jaob  1427  merco1  1716  19.21v  1943  19.39  1989  moimi  2540  r19.30OLD  3122  r19.37  3260  axrep2  5289  dmcosseq  5973  fliftfun  7309  tz7.48lem  8441  ssfi  9173  ac6sfi  9287  frfi  9288  domunfican  9320  iunfi  9340  finsschain  9359  cantnfval2  9664  cantnflt  9667  cnfcom  9695  kmlem1  10145  kmlem13  10157  axpowndlem2  10593  wunfi  10716  ingru  10810  xrub  13291  hashf1lem2  14417  caubnd  15305  fsum2d  15717  fsumabs  15747  fsumrlim  15757  fsumo1  15758  fsumiun  15767  fprod2d  15925  ablfac1eulem  19942  mplcoe1  21592  mplcoe5  21595  mdetunilem9  22122  t1t0  22852  fiuncmp  22908  ptcmpfi  23317  isfil2  23360  fsumcn  24386  ovolfiniun  25018  finiunmbl  25061  volfiniun  25064  itgfsum  25344  dvmptfsum  25492  pntrsumbnd  27069  mulsproplem12  27586  mulsproplem13  27587  mulsproplem14  27588  nmounbseqi  30061  nmounbseqiALT  30062  isch3  30525  dmdmd  31584  mdslmd1lem2  31610  sumdmdi  31704  dmdbr4ati  31705  dmdbr6ati  31707  gsumle  32273  gsumvsca1  32402  gsumvsca2  32403  pwsiga  33159  bnj1533  33894  bnj110  33900  bnj1523  34113  dfon2lem8  34793  meran1  35344  bj-stabpeirce  35478  bj-bi3ant  35515  bj-ssbid2ALT  35588  bj-spnfw  35595  bj-spst  35615  bj-19.23bit  35617  wl-syls2  36426  heibor1lem  36725  isltrn2N  39039  cdlemefrs32fva  39319  fiinfi  42372  con3ALT2  43339  alrim3con13v  43342  islinindfis  47178  setrec1lem4  47783