Theorem imim1i 64

Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Inference associated with imim1 84. Its associated inference is syl 18. (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 23	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	imim12i 63	1 ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  jarr  107  jarl  126  impt  180  pm3.41  498  pm3.42  499  pm2.67-2  905  jaob  976  merco1  1746  19.21v  1972  19.39  2023  r19.37  3266  axrep2  5235  axprlem1  5385  axprlem4  5388  axprg  5395  dmcosseq  5960  dmcosseqOLD  5961  fliftfun  7318  tz7.48lemOLD  8444  ssfi  9181  ac6sfi  9268  frfi  9269  domunfican  9306  iunfi  9325  finsschain  9341  cantnfval2  9663  cantnflt  9666  cnfcom  9694  setrec1lem4  9964  kmlem1  10222  kmlem13  10234  axpowndlem2  10676  wunfi  10799  ingru  10893  xrub  13435  hashf1lem2  14594  caubnd  15519  fsum2d  15930  fsumabs  15961  fsumrlim  15971  fsumo1  15972  fsumiun  15981  fprod2d  16141  ablfac1eulem  20281  gsumle  20352  mplcoe1  22339  mplcoe5  22342  mdetunilem9  22928  t1t0  23659  fiuncmp  23715  ptcmpfi  24125  isfil2  24168  fsumcn  25184  ovolfiniun  25815  finiunmbl  25858  volfiniun  25861  itgfsum  26140  dvmptfsum  26288  pntrsumbnd  27886  mulsproplem12  28506  mulsproplem13  28507  mulsproplem14  28508  nmounbseqi  31372  nmounbseqiALT  31373  isch3  31836  dmdmd  32895  mdslmd1lem2  32921  sumdmdi  33015  dmdbr4ati  33016  dmdbr6ati  33018  gsumvsca1  33780  gsumvsca2  33781  pwsiga  34755  bnj1533  35475  bnj110  35481  bnj1523  35694  axpowg2  35798  axpowg3  35799  dfon2lem8  36532  meran1  37179  axtco1from2  37243  dfttc4lem2  37297  mh-setindnd  37305  bj-stabpeirce  37401  bj-bi3ant  37439  bj-ssbid2ALT  37542  bj-spnfw  37550  bj-spst  37571  bj-19.23bit  37573  wl-syls2  38421  findcard4  38612  heibor1lem  38723  disjimrmoeqec  39720  isltrn2N  41157  cdlemefrs32fva  41437  fiinfi  44558  con3ALT2  45498  alrim3con13v  45501  islinindfis  49530