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  123  impt  171  pm3.41  485  pm3.42  486  pm2.67-2  875  jaob  944  3jaob  1406  merco1  1676  19.21v  1898  19.39  1941  moimi  2550  r19.30  3273  r19.37  3278  axrep2  5046  dmcosseq  5679  fliftfun  6882  tz7.48lem  7873  ac6sfi  8549  frfi  8550  domunfican  8578  iunfi  8599  finsschain  8618  cantnfval2  8918  cantnflt  8921  cnfcom  8949  kmlem1  9362  kmlem13  9374  axpowndlem2  9810  wunfi  9933  ingru  10027  xrub  12514  hashf1lem2  13617  caubnd  14569  fsum2d  14976  fsumabs  15006  fsumrlim  15016  fsumo1  15017  fsumiun  15026  fprod2d  15185  ablfac1eulem  18934  mplcoe1  19949  mplcoe5  19952  mdetunilem9  20923  t1t0  21650  fiuncmp  21706  ptcmpfi  22115  isfil2  22158  fsumcn  23171  ovolfiniun  23795  finiunmbl  23838  volfiniun  23841  itgfsum  24120  dvmptfsum  24265  pntrsumbnd  25834  nmounbseqi  28321  nmounbseqiALT  28322  isch3  28787  dmdmd  29848  mdslmd1lem2  29874  sumdmdi  29968  dmdbr4ati  29969  dmdbr6ati  29971  gsumle  30478  gsumvsca1  30481  gsumvsca2  30482  pwsiga  30991  bnj1533  31732  bnj110  31738  bnj1523  31949  dfon2lem8  32495  meran1  33219  bj-bi3ant  33378  bj-ssbid2ALT  33443  bj-spnfw  33452  bj-spst  33472  bj-19.23bit  33474  bj-axrep2  33559  wl-syls2  34125  heibor1lem  34477  isltrn2N  36649  cdlemefrs32fva  36929  fiinfi  39239  con3ALT2  40227  alrim3con13v  40230  islinindfis  43811  setrec1lem4  44100