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  5284  dmcosseq  5967  fliftfun  7296  tz7.48lem  8428  ssfi  9161  ac6sfi  9275  frfi  9276  domunfican  9308  iunfi  9328  finsschain  9347  cantnfval2  9651  cantnflt  9654  cnfcom  9682  kmlem1  10132  kmlem13  10144  axpowndlem2  10580  wunfi  10703  ingru  10797  xrub  13278  hashf1lem2  14404  caubnd  15292  fsum2d  15704  fsumabs  15734  fsumrlim  15744  fsumo1  15745  fsumiun  15754  fprod2d  15912  ablfac1eulem  19925  mplcoe1  21560  mplcoe5  21563  mdetunilem9  22091  t1t0  22821  fiuncmp  22877  ptcmpfi  23286  isfil2  23329  fsumcn  24355  ovolfiniun  24987  finiunmbl  25030  volfiniun  25033  itgfsum  25313  dvmptfsum  25461  pntrsumbnd  27036  mulsproplem12  27550  mulsproplem13  27551  mulsproplem14  27552  nmounbseqi  29995  nmounbseqiALT  29996  isch3  30459  dmdmd  31518  mdslmd1lem2  31544  sumdmdi  31638  dmdbr4ati  31639  dmdbr6ati  31641  gsumle  32213  gsumvsca1  32342  gsumvsca2  32343  pwsiga  33059  bnj1533  33794  bnj110  33800  bnj1523  34013  dfon2lem8  34693  meran1  35201  bj-stabpeirce  35335  bj-bi3ant  35372  bj-ssbid2ALT  35445  bj-spnfw  35452  bj-spst  35472  bj-19.23bit  35474  wl-syls2  36283  heibor1lem  36583  isltrn2N  38897  cdlemefrs32fva  39177  fiinfi  42195  con3ALT2  43162  alrim3con13v  43165  islinindfis  46970  setrec1lem4  47575