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  1713  19.21v  1939  19.39  1990  moimi  2545  r19.37  3249  axrep2  5257  axprlem4  5401  dmcosseq  5961  dmcosseqOLD  5962  fliftfun  7310  tz7.48lem  8460  ssfi  9192  ac6sfi  9297  frfi  9298  domunfican  9338  iunfi  9360  finsschain  9376  cantnfval2  9688  cantnflt  9691  cnfcom  9719  kmlem1  10170  kmlem13  10182  axpowndlem2  10617  wunfi  10740  ingru  10834  xrub  13333  hashf1lem2  14479  caubnd  15382  fsum2d  15792  fsumabs  15822  fsumrlim  15832  fsumo1  15833  fsumiun  15842  fprod2d  16002  ablfac1eulem  20060  mplcoe1  22000  mplcoe5  22003  mdetunilem9  22563  t1t0  23291  fiuncmp  23347  ptcmpfi  23756  isfil2  23799  fsumcn  24817  ovolfiniun  25459  finiunmbl  25502  volfiniun  25505  itgfsum  25785  dvmptfsum  25936  pntrsumbnd  27534  mulsproplem12  28087  mulsproplem13  28088  mulsproplem14  28089  nmounbseqi  30763  nmounbseqiALT  30764  isch3  31227  dmdmd  32286  mdslmd1lem2  32312  sumdmdi  32406  dmdbr4ati  32407  dmdbr6ati  32409  gsumle  33097  gsumvsca1  33228  gsumvsca2  33229  pwsiga  34166  bnj1533  34888  bnj110  34894  bnj1523  35107  dfon2lem8  35813  meran1  36434  bj-stabpeirce  36577  bj-bi3ant  36612  bj-ssbid2ALT  36686  bj-spnfw  36693  bj-spst  36712  bj-19.23bit  36714  wl-syls2  37532  heibor1lem  37838  isltrn2N  40144  cdlemefrs32fva  40424  fiinfi  43564  con3ALT2  44522  alrim3con13v  44525  islinindfis  48392  setrec1lem4  49521