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 ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒))

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  107  jarl  126  impt  180  pm3.41  497  pm3.42  498  pm2.67-2  904  jaob  976  merco1  1743  19.21v  1969  19.39  2020  r19.37  3268  axrep2  5242  axprlem1  5396  axprlem4  5399  axprg  5410  dmcosseq  5970  dmcosseqOLD  5971  fliftfun  7312  tz7.48lem  8429  ssfi  9158  ac6sfi  9245  frfi  9246  domunfican  9282  iunfi  9301  finsschain  9317  cantnfval2  9639  cantnflt  9642  cnfcom  9670  kmlem1  10135  kmlem13  10147  axpowndlem2  10584  wunfi  10707  ingru  10801  xrub  13339  hashf1lem2  14495  caubnd  15412  fsum2d  15824  fsumabs  15855  fsumrlim  15865  fsumo1  15866  fsumiun  15875  fprod2d  16037  ablfac1eulem  20145  gsumle  20216  mplcoe1  22169  mplcoe5  22172  mdetunilem9  22758  t1t0  23486  fiuncmp  23542  ptcmpfi  23951  isfil2  23994  fsumcn  25010  ovolfiniun  25641  finiunmbl  25684  volfiniun  25687  itgfsum  25967  dvmptfsum  26115  pntrsumbnd  27711  mulsproplem12  28301  mulsproplem13  28302  mulsproplem14  28303  nmounbseqi  31110  nmounbseqiALT  31111  isch3  31574  dmdmd  32633  mdslmd1lem2  32659  sumdmdi  32753  dmdbr4ati  32754  dmdbr6ati  32756  gsumvsca1  33527  gsumvsca2  33528  pwsiga  34501  bnj1533  35221  bnj110  35227  bnj1523  35440  axpowg2  35541  axpowg3  35542  dfon2lem8  36261  meran1  36903  axtco1from2  36967  dfttc4lem2  37021  mh-setindnd  37029  bj-stabpeirce  37125  bj-bi3ant  37163  bj-ssbid2ALT  37266  bj-spnfw  37274  bj-spst  37295  bj-19.23bit  37297  wl-syls2  38145  heibor1lem  38441  disjimrmoeqec  39438  isltrn2N  40875  cdlemefrs32fva  41155  fiinfi  44282  con3ALT2  45222  alrim3con13v  45225  islinindfis  49212  setrec1lem4  50451