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  27583  mulsproplem13  27584  mulsproplem14  27585  nmounbseqi  30030  nmounbseqiALT  30031  isch3  30494  dmdmd  31553  mdslmd1lem2  31579  sumdmdi  31673  dmdbr4ati  31674  dmdbr6ati  31676  gsumle  32242  gsumvsca1  32371  gsumvsca2  32372  pwsiga  33128  bnj1533  33863  bnj110  33869  bnj1523  34082  dfon2lem8  34762  meran1  35296  bj-stabpeirce  35430  bj-bi3ant  35467  bj-ssbid2ALT  35540  bj-spnfw  35547  bj-spst  35567  bj-19.23bit  35569  wl-syls2  36378  heibor1lem  36677  isltrn2N  38991  cdlemefrs32fva  39271  fiinfi  42324  con3ALT2  43291  alrim3con13v  43294  islinindfis  47130  setrec1lem4  47735