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  891  jaob  963  3jaobOLD  1429  merco1  1713  19.21v  1939  19.39  1990  moimi  2538  r19.37  3238  axrep2  5232  axprlem4  5376  dmcosseq  5929  dmcosseqOLD  5930  fliftfun  7269  tz7.48lem  8386  ssfi  9114  ac6sfi  9207  frfi  9208  domunfican  9248  iunfi  9270  finsschain  9286  cantnfval2  9598  cantnflt  9601  cnfcom  9629  kmlem1  10080  kmlem13  10092  axpowndlem2  10527  wunfi  10650  ingru  10744  xrub  13248  hashf1lem2  14397  caubnd  15301  fsum2d  15713  fsumabs  15743  fsumrlim  15753  fsumo1  15754  fsumiun  15763  fprod2d  15923  ablfac1eulem  19980  mplcoe1  21920  mplcoe5  21923  mdetunilem9  22483  t1t0  23211  fiuncmp  23267  ptcmpfi  23676  isfil2  23719  fsumcn  24737  ovolfiniun  25378  finiunmbl  25421  volfiniun  25424  itgfsum  25704  dvmptfsum  25855  pntrsumbnd  27453  mulsproplem12  28006  mulsproplem13  28007  mulsproplem14  28008  nmounbseqi  30679  nmounbseqiALT  30680  isch3  31143  dmdmd  32202  mdslmd1lem2  32228  sumdmdi  32322  dmdbr4ati  32323  dmdbr6ati  32325  gsumle  33011  gsumvsca1  33152  gsumvsca2  33153  pwsiga  34093  bnj1533  34815  bnj110  34821  bnj1523  35034  dfon2lem8  35751  meran1  36372  bj-stabpeirce  36515  bj-bi3ant  36550  bj-ssbid2ALT  36624  bj-spnfw  36631  bj-spst  36650  bj-19.23bit  36652  wl-syls2  37470  heibor1lem  37776  isltrn2N  40087  cdlemefrs32fva  40367  fiinfi  43535  con3ALT2  44493  alrim3con13v  44496  islinindfis  48411  setrec1lem4  49652