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  impt  169  jarl  175  pm2.67-2  416  pm3.41  581  pm3.42  582  jaob  839  3jaob  1430  merco1  1678  19.21v  1908  19.39  1956  r19.37  3115  axrep2  4806  dmcosseq  5419  fliftfun  6602  tz7.48lem  7581  ac6sfi  8245  frfi  8246  domunfican  8274  iunfi  8295  finsschain  8314  cantnfval2  8604  cantnflt  8607  cnfcom  8635  kmlem1  9010  kmlem13  9022  axpowndlem2  9458  wunfi  9581  ingru  9675  xrub  12180  hashf1lem2  13278  caubnd  14142  fsum2d  14546  fsumabs  14577  fsumrlim  14587  fsumo1  14588  fsumiun  14597  fprod2d  14755  ablfac1eulem  18517  mplcoe1  19513  mplcoe5  19516  mdetunilem9  20474  t1t0  21200  fiuncmp  21255  ptcmpfi  21664  isfil2  21707  fsumcn  22720  ovolfiniun  23315  finiunmbl  23358  volfiniun  23361  itgfsum  23638  dvmptfsum  23783  pntrsumbnd  25300  nmounbseqi  27760  nmounbseqiALT  27761  isch3  28226  dmdmd  29287  mdslmd1lem2  29313  sumdmdi  29407  dmdbr4ati  29408  dmdbr6ati  29410  gsumle  29907  gsumvsca1  29910  gsumvsca2  29911  pwsiga  30321  bnj1533  31048  bnj110  31054  bnj1523  31265  dfon2lem8  31819  meran1  32535  bj-bi3ant  32699  bj-ssbid2ALT  32771  bj-spnfw  32783  bj-spst  32804  bj-19.23bit  32806  bj-axrep2  32914  wl-syls2  33422  heibor1lem  33738  isltrn2N  35724  cdlemefrs32fva  36005  fiinfi  38195  con3ALT2  39053  alrim3con13v  39060  islinindfis  42563  setrec1lem4  42762