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  888  jaob  958  3jaob  1424  merco1  1717  19.21v  1943  19.39  1989  moimi  2545  r19.30OLD  3266  r19.37  3270  axrep2  5208  dmcosseq  5871  fliftfun  7163  tz7.48lem  8242  ssfi  8918  ac6sfi  8988  frfi  8989  domunfican  9017  iunfi  9037  finsschain  9056  cantnfval2  9357  cantnflt  9360  cnfcom  9388  kmlem1  9837  kmlem13  9849  axpowndlem2  10285  wunfi  10408  ingru  10502  xrub  12975  hashf1lem2  14098  caubnd  14998  fsum2d  15411  fsumabs  15441  fsumrlim  15451  fsumo1  15452  fsumiun  15461  fprod2d  15619  ablfac1eulem  19590  mplcoe1  21148  mplcoe5  21151  mdetunilem9  21677  t1t0  22407  fiuncmp  22463  ptcmpfi  22872  isfil2  22915  fsumcn  23939  ovolfiniun  24570  finiunmbl  24613  volfiniun  24616  itgfsum  24896  dvmptfsum  25044  pntrsumbnd  26619  nmounbseqi  29040  nmounbseqiALT  29041  isch3  29504  dmdmd  30563  mdslmd1lem2  30589  sumdmdi  30683  dmdbr4ati  30684  dmdbr6ati  30686  gsumle  31252  gsumvsca1  31381  gsumvsca2  31382  pwsiga  31998  bnj1533  32732  bnj110  32738  bnj1523  32951  dfon2lem8  33672  meran1  34527  bj-stabpeirce  34661  bj-bi3ant  34698  bj-ssbid2ALT  34771  bj-spnfw  34778  bj-spst  34798  bj-19.23bit  34800  wl-syls2  35595  heibor1lem  35894  isltrn2N  38061  cdlemefrs32fva  38341  fiinfi  41069  con3ALT2  42039  alrim3con13v  42042  islinindfis  45678  setrec1lem4  46282