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  1745  19.21v  1971  19.39  2022  r19.37  3265  axrep2  5234  axprlem1  5384  axprlem4  5387  axprg  5394  dmcosseq  5959  dmcosseqOLD  5960  fliftfun  7321  tz7.48lemOLD  8455  ssfi  9192  ac6sfi  9279  frfi  9280  domunfican  9317  iunfi  9336  finsschain  9352  cantnfval2  9674  cantnflt  9677  cnfcom  9705  setrec1lem4  9975  kmlem1  10233  kmlem13  10245  axpowndlem2  10687  wunfi  10810  ingru  10904  xrub  13446  hashf1lem2  14605  caubnd  15532  fsum2d  15943  fsumabs  15974  fsumrlim  15984  fsumo1  15985  fsumiun  15994  fprod2d  16154  ablfac1eulem  20294  gsumle  20365  mplcoe1  22352  mplcoe5  22355  mdetunilem9  22941  t1t0  23672  fiuncmp  23728  ptcmpfi  24138  isfil2  24181  fsumcn  25197  ovolfiniun  25828  finiunmbl  25871  volfiniun  25874  itgfsum  26153  dvmptfsum  26301  pntrsumbnd  27899  mulsproplem12  28519  mulsproplem13  28520  mulsproplem14  28521  nmounbseqi  31385  nmounbseqiALT  31386  isch3  31849  dmdmd  32908  mdslmd1lem2  32934  sumdmdi  33028  dmdbr4ati  33029  dmdbr6ati  33031  gsumvsca1  33834  gsumvsca2  33835  pwsiga  34809  bnj1533  35529  bnj110  35535  bnj1523  35748  axpowg2  35872  axpowg3  35873  dfon2lem8  36645  meran1  37292  axtco1from2  37356  dfttc4lem2  37410  mh-setindnd  37418  bj-stabpeirce  37514  bj-bi3ant  37552  bj-ssbid2ALT  37655  bj-spnfw  37663  bj-spst  37684  bj-19.23bit  37686  wl-syls2  38535  findcard4  38726  heibor1lem  38837  disjimrmoeqec  39834  isltrn2N  41271  cdlemefrs32fva  41551  fiinfi  44668  con3ALT2  45607  alrim3con13v  45610  islinindfis  49655