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  180  pm3.41  495  pm3.42  496  pm2.67-2  888  jaob  958  3jaob  1422  merco1  1714  19.21v  1940  19.39  1991  moimi  2627  r19.30  3340  r19.37  3345  axrep2  5195  dmcosseq  5846  fliftfun  7067  tz7.48lem  8079  ac6sfi  8764  frfi  8765  domunfican  8793  iunfi  8814  finsschain  8833  cantnfval2  9134  cantnflt  9137  cnfcom  9165  kmlem1  9578  kmlem13  9590  axpowndlem2  10022  wunfi  10145  ingru  10239  xrub  12708  hashf1lem2  13817  caubnd  14720  fsum2d  15128  fsumabs  15158  fsumrlim  15168  fsumo1  15169  fsumiun  15178  fprod2d  15337  ablfac1eulem  19196  mplcoe1  20248  mplcoe5  20251  mdetunilem9  21231  t1t0  21958  fiuncmp  22014  ptcmpfi  22423  isfil2  22466  fsumcn  23480  ovolfiniun  24104  finiunmbl  24147  volfiniun  24150  itgfsum  24429  dvmptfsum  24574  pntrsumbnd  26144  nmounbseqi  28556  nmounbseqiALT  28557  isch3  29020  dmdmd  30079  mdslmd1lem2  30105  sumdmdi  30199  dmdbr4ati  30200  dmdbr6ati  30202  gsumle  30727  gsumvsca1  30856  gsumvsca2  30857  pwsiga  31391  bnj1533  32126  bnj110  32132  bnj1523  32345  dfon2lem8  33037  meran1  33761  bj-stabpeirce  33891  bj-bi3ant  33925  bj-ssbid2ALT  33998  bj-spnfw  34005  bj-spst  34025  bj-19.23bit  34027  wl-syls2  34751  heibor1lem  35089  isltrn2N  37258  cdlemefrs32fva  37538  fiinfi  39939  con3ALT2  40871  alrim3con13v  40874  islinindfis  44511  setrec1lem4  44800