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  1714  19.21v  1940  19.39  1991  moimi  2542  r19.37  3236  axrep2  5224  axprlem4  5368  dmcosseq  5924  dmcosseqOLD  5925  dmcosseqOLDOLD  5926  fliftfun  7255  tz7.48lem  8369  ssfi  9093  ac6sfi  9179  frfi  9180  domunfican  9217  iunfi  9238  finsschain  9254  cantnfval2  9570  cantnflt  9573  cnfcom  9601  kmlem1  10053  kmlem13  10065  axpowndlem2  10500  wunfi  10623  ingru  10717  xrub  13218  hashf1lem2  14370  caubnd  15273  fsum2d  15685  fsumabs  15715  fsumrlim  15725  fsumo1  15726  fsumiun  15735  fprod2d  15895  ablfac1eulem  19994  gsumle  20065  mplcoe1  21983  mplcoe5  21986  mdetunilem9  22555  t1t0  23283  fiuncmp  23339  ptcmpfi  23748  isfil2  23791  fsumcn  24808  ovolfiniun  25449  finiunmbl  25492  volfiniun  25495  itgfsum  25775  dvmptfsum  25926  pntrsumbnd  27524  mulsproplem12  28086  mulsproplem13  28087  mulsproplem14  28088  nmounbseqi  30778  nmounbseqiALT  30779  isch3  31242  dmdmd  32301  mdslmd1lem2  32327  sumdmdi  32421  dmdbr4ati  32422  dmdbr6ati  32424  gsumvsca1  33236  gsumvsca2  33237  pwsiga  34215  bnj1533  34936  bnj110  34942  bnj1523  35155  dfon2lem8  35904  meran1  36527  bj-stabpeirce  36670  bj-bi3ant  36705  bj-ssbid2ALT  36780  bj-spnfw  36787  bj-spst  36806  bj-19.23bit  36808  wl-syls2  37626  heibor1lem  37922  isltrn2N  40292  cdlemefrs32fva  40572  fiinfi  43730  con3ALT2  44687  alrim3con13v  44690  islinindfis  48611  setrec1lem4  49851