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  1974  19.39  2025  r19.37  3269  axrep2  5241  axprlem1  5392  axprlem4  5395  axprg  5402  dmcosseq  5972  dmcosseqOLD  5973  fliftfun  7351  tz7.48lemOLD  8489  ssfi  9226  ac6sfi  9313  frfi  9314  domunfican  9351  iunfi  9370  finsschain  9386  cantnfval2  9707  cantnflt  9710  cnfcom  9738  setrec1lem4  10008  kmlem1  10268  kmlem13  10280  axpowndlem2  10722  wunfi  10845  ingru  10939  xrub  13482  hashf1lem2  14642  caubnd  15570  fsum2d  15981  fsumabs  16012  fsumrlim  16022  fsumo1  16023  fsumiun  16032  fprod2d  16192  ablfac1eulem  20339  gsumle  20410  mplcoe1  22401  mplcoe5  22404  mdetunilem9  22990  t1t0  23721  fiuncmp  23777  ptcmpfi  24187  isfil2  24230  fsumcn  25246  ovolfiniun  25877  finiunmbl  25920  volfiniun  25923  itgfsum  26202  dvmptfsum  26350  pntrsumbnd  27950  mulsproplem12  28570  mulsproplem13  28571  mulsproplem14  28572  nmounbseqi  31436  nmounbseqiALT  31437  isch3  31900  dmdmd  32959  mdslmd1lem2  32985  sumdmdi  33079  dmdbr4ati  33080  dmdbr6ati  33082  gsumvsca1  33886  gsumvsca2  33887  pwsiga  34873  bnj1533  35593  bnj110  35599  bnj1523  35812  axpowg2  35956  axpowg3  35957  dfon2lem8  36767  meran1  37414  axtco1from2  37478  dfttc4lem2  37532  mh-setindnd  37540  bj-stabpeirce  37636  bj-bi3ant  37674  bj-ssbid2ALT  37777  bj-spnfw  37785  bj-spst  37806  bj-19.23bit  37808  wl-syls2  38709  findcard4  38900  heibor1lem  39009  disjimrmoeqec  40006  isltrn2N  41443  cdlemefrs32fva  41723  fiinfi  44835  con3ALT2  45773  alrim3con13v  45776  islinindfis  49892