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  7320  tz7.48lemOLD  8451  ssfi  9188  ac6sfi  9275  frfi  9276  domunfican  9313  iunfi  9332  finsschain  9348  cantnfval2  9670  cantnflt  9673  cnfcom  9701  setrec1lem4  9971  kmlem1  10229  kmlem13  10241  axpowndlem2  10683  wunfi  10806  ingru  10900  xrub  13442  hashf1lem2  14601  caubnd  15526  fsum2d  15937  fsumabs  15968  fsumrlim  15978  fsumo1  15979  fsumiun  15988  fprod2d  16148  ablfac1eulem  20288  gsumle  20359  mplcoe1  22346  mplcoe5  22349  mdetunilem9  22935  t1t0  23666  fiuncmp  23722  ptcmpfi  24132  isfil2  24175  fsumcn  25191  ovolfiniun  25822  finiunmbl  25865  volfiniun  25868  itgfsum  26147  dvmptfsum  26295  pntrsumbnd  27893  mulsproplem12  28513  mulsproplem13  28514  mulsproplem14  28515  nmounbseqi  31379  nmounbseqiALT  31380  isch3  31843  dmdmd  32902  mdslmd1lem2  32928  sumdmdi  33022  dmdbr4ati  33023  dmdbr6ati  33025  gsumvsca1  33787  gsumvsca2  33788  pwsiga  34762  bnj1533  35482  bnj110  35488  bnj1523  35701  axpowg2  35815  axpowg3  35816  dfon2lem8  36552  meran1  37199  axtco1from2  37263  dfttc4lem2  37317  mh-setindnd  37325  bj-stabpeirce  37421  bj-bi3ant  37459  bj-ssbid2ALT  37562  bj-spnfw  37570  bj-spst  37591  bj-19.23bit  37593  wl-syls2  38441  findcard4  38632  heibor1lem  38743  disjimrmoeqec  39740  isltrn2N  41177  cdlemefrs32fva  41457  fiinfi  44573  con3ALT2  45512  alrim3con13v  45515  islinindfis  49560