Theorem sylc 62

Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)

Hypotheses

Ref	Expression
sylc.1	⊢ (𝜑 → 𝜓)
sylc.2	⊢ (𝜑 → 𝜒)
sylc.3	⊢ (𝜓 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylc	⊢ (𝜑 → 𝜃)

Proof of Theorem sylc

Step	Hyp	Ref	Expression
1		sylc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylc.3	. . 3 ⊢ (𝜓 → (𝜒 → 𝜃))
4	1, 2, 3	syl2im 38	. 2 ⊢ (𝜑 → (𝜑 → 𝜃))
5	4	pm2.43i 49	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:  syl3c  63  mpsyl  65  imp  124  2thd  175  jca  306  syl2anc  411  jc  656  jcnd  658  annimdc  946  pm4.55dc  947  orandc  948  dn1dc  969  syl2an23an  1336  xordidc  1444  nfimd  1634  exlimd2  1644  elex22  2829  elex2  2830  spcimdv  2901  spcimedv  2903  spcedv  2906  rspcdva  2926  elabd  2962  spsbcd  3055  opth  4353  euotd  4371  ssorduni  4609  tfisi  4709  omsinds  4744  nnpredcl  4745  sotri2  5160  sotri3  5161  unielrel  5290  funmo  5367  fnfvima  5921  resfvresima  5923  fliftfun  5969  fliftval  5973  riota5f  6030  riotass2  6032  fovcld  6158  oprssdmm  6365  funsssuppss  6458  tfrlem5  6545  tfrlemibxssdm  6558  tfrlemibfn  6559  tfrlemiex  6562  tfr1onlemsucfn  6571  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlembfn  6575  tfr1onlemex  6578  tfr1onlemres  6580  tfrcllemsucfn  6584  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllembfn  6588  tfrcllemex  6591  tfrcllemres  6593  tfrcl  6595  rdgisucinc  6616  frecabex  6629  frecabcl  6630  nntr2  6736  ertr  6782  qliftlem  6847  th3q  6874  resixp  6968  f1dom2g  6995  dom3d  7013  domssr  7017  en1  7039  xpdom3m  7085  xpf1o  7097  phplem4dom  7116  phpm  7120  phpelm  7121  findcard  7145  finexdc  7160  fiintim  7191  fisseneq  7195  ssfirab  7197  opabfi  7200  f1dmvrnfibi  7211  iunfidisj  7213  fidcenumlemrk  7224  dcfi  7268  2omapfi  7271  suplub2ti  7292  supelti  7293  ordiso2  7326  caseinl  7382  caseinr  7383  djudom  7384  difinfsn  7391  difinfinf  7392  ctm  7400  enumct  7406  nnnninfeq  7419  ismkvnex  7446  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  acfun  7514  exmidontriimlem2  7529  exmidontriimlem3  7530  exmidapne  7574  cc2lem  7580  cc3  7582  recexnq  7705  ltbtwnnqq  7730  addnnnq0  7764  mulnnnq0  7765  prarloclemn  7814  prarloc  7818  distrlem1prl  7897  distrlem1pru  7898  distrlem4prl  7899  distrlem4pru  7900  ltexprlemrl  7925  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  addsrpr  8060  mulsrpr  8061  map2psrprg  8120  axpre-suploclemres  8216  lemul12a  9136  lemulge11  9140  sup3exmid  9231  nngt0  9262  nn0ge0  9521  nn0ge2m1nn  9560  zletric  9621  zlelttric  9622  nn0n0n1ge2b  9657  nn0ind-raph  9695  supinfneg  9927  infsupneg  9928  infregelbex  9930  rpge0  9999  fz0fzelfz0  10461  fz0fzdiffz0  10464  ige2m2fzo  10543  elfzodifsumelfzo  10546  elfzom1elp1fzo  10547  exfzdc  10586  zsupcllemstep  10589  infssuzex  10593  qletric  10601  qlelttric  10602  rebtwn2zlemshrink  10613  frecuzrdgtcl  10774  frecuzrdg0  10775  frecuzrdgfunlem  10781  frecuzrdg0t  10784  frecuzrdgsuctlem  10785  frecfzennn  10788  seq3f1olemstep  10876  expcl2lemap  10913  leexp1a  10956  expnbnd  11025  faclbnd  11103  faclbnd6  11106  facavg  11108  fihasheqf1oi  11150  fihashf1rn  11151  fihashss  11181  fiubm  11195  seq3coll  11214  wrdsymb0  11257  wrdlenge2n0  11260  ccatsymb  11290  pfxnd  11381  pfxccat1  11394  swrdpfx  11399  pfxpfx  11400  wrd2ind  11415  pfxccatin12  11425  pfxccat3  11426  swrdccat  11427  pfxccatpfx1  11428  pfxccatpfx2  11429  swrdccatin1d  11435  pfxccatin12d  11437  resqrexlemdecn  11697  qabsor  11760  cau3lem  11799  xrmaxiflemab  11932  xrmaxadd  11946  climcn2  11994  sumeq2  12044  sumrbdclem  12063  summodclem3  12066  summodclem2a  12067  zsumdc  12070  fsumgcl  12072  fsum3  12073  isumss  12077  fsumadd  12092  fsum2dlemstep  12120  fisum0diag2  12133  fsummulc2  12134  modfsummodlemstep  12143  fsumabs  12151  fsumrelem  12157  fsumiun  12163  isumshft  12176  mertenslem2  12222  prodeq2  12243  prodrbdclem  12257  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  fprodmul  12277  fprodconst  12306  fprodap0  12307  fprod2dlemstep  12308  fprodrec  12315  fprodsplit1f  12320  fprodap0f  12322  fprodle  12326  sin02gt0  12450  efieq1re  12458  p1modz1  12480  dvdsleabs2  12532  4dvdseven  12603  bitsfzo  12641  bitsinv1lem  12647  gcdeq0  12673  rppwr  12724  uzwodc  12733  algfx  12749  eucalgcvga  12755  lcmmndc  12759  lcmeq0  12768  qredeq  12793  isprm3  12815  rpexp  12850  sqpweven  12872  2sqpwodd  12873  phicl2  12911  phibnd  12914  phiprmpw  12919  fermltl  12931  pythagtriplem4  12966  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem12  12973  pythagtriplem13  12974  pythagtriplem14  12975  pythagtriplem16  12977  pcdvdsb  13018  pc2dvds  13028  difsqpwdvds  13036  pcmpt  13041  pcmptdvds  13043  fldivp1  13046  prmpwdvds  13053  infpnlem1  13057  1arith  13065  4sqlem11  13099  ennnfonelemk  13151  ennnfonelemhom  13166  ennnfonelemrnh  13167  ennnfonelemf1  13169  ctinf  13181  ctiunctlemudc  13188  ctiunctlemf  13189  nninfdclemp1  13201  strslfvd  13254  strslfv2d  13255  strslssd  13259  imasival  13519  imasbas  13520  imasplusg  13521  imasaddfnlemg  13527  imasaddvallemg  13528  qusaddvallemg  13546  qusaddflemg  13547  qusaddval  13548  qusaddf  13549  qusmulval  13550  qusmulf  13551  lidrididd  13595  gsumfzval  13604  sgrpidmndm  13633  gsumfzz  13708  qusgrp2  13830  mulgnegnn  13849  eqgen  13944  rinvmod  14026  gsumfzconst  14058  qusrng  14102  srgdilem  14113  ringdilem  14156  qusring2  14210  lssintclm  14532  gsumfzfsumlemm  14735  mplsubgfilemm  14853  eltg3  14922  iuncld  14980  cnss2  15092  txcnp  15136  uptx  15139  xblm  15282  metss  15359  fsumcncntop  15432  rescncf  15446  dedekindeulemlu  15486  suplociccex  15490  dedekindicclemlu  15495  dedekindicc  15498  ivthdec  15509  limccnp2lem  15541  dvaddxx  15568  dvmulxx  15569  dvrecap  15578  reeff1olem  15636  perfectlem2  15868  lgsval  15877  lgsfvalg  15878  lgsfcl2  15879  lgscllem  15880  lgsval2lem  15883  lgsneg  15897  lgsdir2  15906  lgsdir  15908  lgsdi  15910  lgsne0  15911  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem0c  15924  m1lgs  15958  2lgslem1  15964  2lgs  15977  2lgsoddprm  15986  2sqlem6  15993  incistruhgr  16085  upgredg  16139  uhgr2edg  16201  usgriedgdomord  16220  wlkpropg  16319  wlkvtxeledgg  16339  wlk2f  16346  clwwlknonccat  16428  clwwlknonex2lem2  16433  eupth2lem3lem4fi  16468  eupth2lem3lem7fi  16469  sumdc2  16571  pwle2  16772  subctctexmid  16774  nninfsellemeq  16792  nnnninfex  16800  exmidsbthrlem  16802  cndcap  16844  gfsump1  16868