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  3265  axrep2  5235  axprlem1  5388  axprlem4  5391  axprg  5402  dmcosseq  5962  dmcosseqOLD  5963  fliftfun  7313  tz7.48lem  8430  ssfi  9167  ac6sfi  9254  frfi  9255  domunfican  9291  iunfi  9310  finsschain  9326  cantnfval2  9648  cantnflt  9651  cnfcom  9679  kmlem1  10153  kmlem13  10165  axpowndlem2  10607  wunfi  10730  ingru  10824  xrub  13364  hashf1lem2  14521  caubnd  15446  fsum2d  15857  fsumabs  15888  fsumrlim  15898  fsumo1  15899  fsumiun  15908  fprod2d  16068  ablfac1eulem  20201  gsumle  20272  mplcoe1  22253  mplcoe5  22256  mdetunilem9  22842  t1t0  23573  fiuncmp  23629  ptcmpfi  24039  isfil2  24082  fsumcn  25098  ovolfiniun  25729  finiunmbl  25772  volfiniun  25775  itgfsum  26054  dvmptfsum  26202  pntrsumbnd  27802  mulsproplem12  28392  mulsproplem13  28393  mulsproplem14  28394  nmounbseqi  31258  nmounbseqiALT  31259  isch3  31722  dmdmd  32781  mdslmd1lem2  32807  sumdmdi  32901  dmdbr4ati  32902  dmdbr6ati  32904  gsumvsca1  33666  gsumvsca2  33667  pwsiga  34640  bnj1533  35361  bnj110  35367  bnj1523  35580  axpowg2  35673  axpowg3  35674  dfon2lem8  36367  meran1  37030  axtco1from2  37094  dfttc4lem2  37148  mh-setindnd  37156  bj-stabpeirce  37252  bj-bi3ant  37290  bj-ssbid2ALT  37393  bj-spnfw  37401  bj-spst  37422  bj-19.23bit  37424  wl-syls2  38272  findcard4  38463  heibor1lem  38559  disjimrmoeqec  39556  isltrn2N  40993  cdlemefrs32fva  41273  fiinfi  44413  con3ALT2  45353  alrim3con13v  45356  islinindfis  49379  setrec1lem4  50616