Theorem imim1i 63

Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Inference associated with imim1 83. Its associated inference is syl 17. (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 22	. 2 ⊢ (𝜒 → 𝜒)
3	1, 2	imim12i 62	1 ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  jarr  106  jarl  125  impt  178  pm3.41  492  pm3.42  493  pm2.67-2  892  jaob  964  3jaobOLD  1430  merco1  1715  19.21v  1941  19.39  1992  r19.37  3240  axrep2  5215  axprlem1  5365  axprlem4  5368  axprg  5379  dmcosseq  5933  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  fliftfun  7267  tz7.48lem  8380  ssfi  9107  ac6sfi  9194  frfi  9195  domunfican  9232  iunfi  9253  finsschain  9269  cantnfval2  9590  cantnflt  9593  cnfcom  9621  kmlem1  10073  kmlem13  10085  axpowndlem2  10521  wunfi  10644  ingru  10738  xrub  13264  hashf1lem2  14418  caubnd  15321  fsum2d  15733  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  fprod2d  15946  ablfac1eulem  20049  gsumle  20120  mplcoe1  22015  mplcoe5  22018  mdetunilem9  22585  t1t0  23313  fiuncmp  23369  ptcmpfi  23778  isfil2  23821  fsumcn  24837  ovolfiniun  25468  finiunmbl  25511  volfiniun  25514  itgfsum  25794  dvmptfsum  25942  pntrsumbnd  27529  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  nmounbseqi  30848  nmounbseqiALT  30849  isch3  31312  dmdmd  32371  mdslmd1lem2  32397  sumdmdi  32491  dmdbr4ati  32492  dmdbr6ati  32494  gsumvsca1  33287  gsumvsca2  33288  pwsiga  34274  bnj1533  34994  bnj110  35000  bnj1523  35213  dfon2lem8  35970  meran1  36593  axtco1from2  36657  dfttc4lem2  36711  mh-setindnd  36719  bj-stabpeirce  36816  bj-bi3ant  36854  bj-ssbid2ALT  36957  bj-spnfw  36965  bj-spst  36986  bj-19.23bit  36988  wl-syls2  37834  heibor1lem  38130  disjimrmoeqec  39129  isltrn2N  40566  cdlemefrs32fva  40846  fiinfi  44000  con3ALT2  44957  alrim3con13v  44960  islinindfis  48925  setrec1lem4  50165