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  3270  axrep2  5243  axprlem1  5396  axprlem4  5399  axprg  5410  dmcosseq  5970  dmcosseqOLD  5971  fliftfun  7316  tz7.48lem  8430  ssfi  9160  ac6sfi  9247  frfi  9248  domunfican  9284  iunfi  9303  finsschain  9319  cantnfval2  9641  cantnflt  9644  cnfcom  9672  kmlem1  10146  kmlem13  10158  axpowndlem2  10594  wunfi  10717  ingru  10811  xrub  13349  hashf1lem2  14506  caubnd  15429  fsum2d  15840  fsumabs  15871  fsumrlim  15881  fsumo1  15882  fsumiun  15891  fprod2d  16053  ablfac1eulem  20167  gsumle  20238  mplcoe1  22217  mplcoe5  22220  mdetunilem9  22806  t1t0  23534  fiuncmp  23590  ptcmpfi  23999  isfil2  24042  fsumcn  25058  ovolfiniun  25689  finiunmbl  25732  volfiniun  25735  itgfsum  26015  dvmptfsum  26163  pntrsumbnd  27759  mulsproplem12  28349  mulsproplem13  28350  mulsproplem14  28351  nmounbseqi  31158  nmounbseqiALT  31159  isch3  31622  dmdmd  32681  mdslmd1lem2  32707  sumdmdi  32801  dmdbr4ati  32802  dmdbr6ati  32804  gsumvsca1  33569  gsumvsca2  33570  pwsiga  34543  bnj1533  35264  bnj110  35270  bnj1523  35483  axpowg2  35576  axpowg3  35577  dfon2lem8  36293  meran1  36955  axtco1from2  37019  dfttc4lem2  37073  mh-setindnd  37081  bj-stabpeirce  37177  bj-bi3ant  37215  bj-ssbid2ALT  37318  bj-spnfw  37326  bj-spst  37347  bj-19.23bit  37349  wl-syls2  38197  heibor1lem  38493  disjimrmoeqec  39490  isltrn2N  40927  cdlemefrs32fva  41207  fiinfi  44332  con3ALT2  45272  alrim3con13v  45275  islinindfis  49262  setrec1lem4  50501