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  493  pm3.42  494  pm2.67-2  889  jaob  959  3jaob  1425  merco1  1716  19.21v  1942  19.39  1988  moimi  2545  r19.30OLD  3269  r19.37  3273  axrep2  5212  dmcosseq  5882  fliftfun  7183  tz7.48lem  8272  ssfi  8956  ac6sfi  9058  frfi  9059  domunfican  9087  iunfi  9107  finsschain  9126  cantnfval2  9427  cantnflt  9430  cnfcom  9458  kmlem1  9906  kmlem13  9918  axpowndlem2  10354  wunfi  10477  ingru  10571  xrub  13046  hashf1lem2  14170  caubnd  15070  fsum2d  15483  fsumabs  15513  fsumrlim  15523  fsumo1  15524  fsumiun  15533  fprod2d  15691  ablfac1eulem  19675  mplcoe1  21238  mplcoe5  21241  mdetunilem9  21769  t1t0  22499  fiuncmp  22555  ptcmpfi  22964  isfil2  23007  fsumcn  24033  ovolfiniun  24665  finiunmbl  24708  volfiniun  24711  itgfsum  24991  dvmptfsum  25139  pntrsumbnd  26714  nmounbseqi  29139  nmounbseqiALT  29140  isch3  29603  dmdmd  30662  mdslmd1lem2  30688  sumdmdi  30782  dmdbr4ati  30783  dmdbr6ati  30785  gsumle  31350  gsumvsca1  31479  gsumvsca2  31480  pwsiga  32098  bnj1533  32832  bnj110  32838  bnj1523  33051  dfon2lem8  33766  meran1  34600  bj-stabpeirce  34734  bj-bi3ant  34771  bj-ssbid2ALT  34844  bj-spnfw  34851  bj-spst  34871  bj-19.23bit  34873  wl-syls2  35668  heibor1lem  35967  isltrn2N  38134  cdlemefrs32fva  38414  fiinfi  41180  con3ALT2  42150  alrim3con13v  42153  islinindfis  45790  setrec1lem4  46396