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  492  pm3.42  493  pm2.67-2  891  jaob  963  3jaobOLD  1428  merco1  1712  19.21v  1938  19.39  1983  moimi  2544  r19.30OLD  3120  r19.37  3261  axrep2  5281  axprlem4  5425  dmcosseq  5986  dmcosseqOLD  5987  fliftfun  7333  tz7.48lem  8482  ssfi  9214  ac6sfi  9321  frfi  9322  domunfican  9362  iunfi  9384  finsschain  9400  cantnfval2  9710  cantnflt  9713  cnfcom  9741  kmlem1  10192  kmlem13  10204  axpowndlem2  10639  wunfi  10762  ingru  10856  xrub  13355  hashf1lem2  14496  caubnd  15398  fsum2d  15808  fsumabs  15838  fsumrlim  15848  fsumo1  15849  fsumiun  15858  fprod2d  16018  ablfac1eulem  20093  mplcoe1  22056  mplcoe5  22059  mdetunilem9  22627  t1t0  23357  fiuncmp  23413  ptcmpfi  23822  isfil2  23865  fsumcn  24895  ovolfiniun  25537  finiunmbl  25580  volfiniun  25583  itgfsum  25863  dvmptfsum  26014  pntrsumbnd  27611  mulsproplem12  28154  mulsproplem13  28155  mulsproplem14  28156  nmounbseqi  30797  nmounbseqiALT  30798  isch3  31261  dmdmd  32320  mdslmd1lem2  32346  sumdmdi  32440  dmdbr4ati  32441  dmdbr6ati  32443  gsumle  33102  gsumvsca1  33233  gsumvsca2  33234  pwsiga  34132  bnj1533  34867  bnj110  34873  bnj1523  35086  dfon2lem8  35792  meran1  36413  bj-stabpeirce  36556  bj-bi3ant  36591  bj-ssbid2ALT  36665  bj-spnfw  36672  bj-spst  36691  bj-19.23bit  36693  wl-syls2  37511  heibor1lem  37817  isltrn2N  40123  cdlemefrs32fva  40403  fiinfi  43591  con3ALT2  44555  alrim3con13v  44558  islinindfis  48371  setrec1lem4  49264