MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylc Structured version   Unicode version

Theorem sylc 59
Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)
Hypotheses
Ref Expression
sylc.1  |-  ( ph  ->  ps )
sylc.2  |-  ( ph  ->  ch )
sylc.3  |-  ( ps 
->  ( ch  ->  th )
)
Assertion
Ref Expression
sylc  |-  ( ph  ->  th )

Proof of Theorem sylc
StepHypRef Expression
1 sylc.1 . . 3  |-  ( ph  ->  ps )
2 sylc.2 . . 3  |-  ( ph  ->  ch )
3 sylc.3 . . 3  |-  ( ps 
->  ( ch  ->  th )
)
41, 2, 3syl2im 37 . 2  |-  ( ph  ->  ( ph  ->  th )
)
54pm2.43i 46 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl3c  60  mpsyl  62  jc  142  2thd  233  jca  520  syl2anc  644  nfimd  1828  ax12OLD  2021  ax12from12o  2235  equid1  2237  elex22  2969  elex2  2970  spcimdv  3035  spsbcd  3176  disjxiun  4211  opth  4437  euotd  4459  wereu  4580  wereu2  4581  tz7.7  4609  reusv2lem3  4728  ssorduni  4768  suceloni  4795  nlimsucg  4824  tfisi  4840  unielrel  5396  funmo  5472  iinpreima  5862  zfrep6  5970  fnfvima  5978  fliftfun  6036  fliftval  6040  weniso  6077  knatar  6082  grprinvlem  6287  grprinvd  6288  caofref  6332  curry1  6440  curry2  6443  fnwelem  6463  riota5f  6576  riotass2  6579  smogt  6631  omeulem1  6827  oeworde  6838  oelimcl  6845  oeeulem  6846  oeeui  6847  nnawordex  6882  oaabs2  6890  ertr  6922  swoso  6938  qliftlem  6987  th3q  7015  resixp  7099  f1dom2g  7127  dom3d  7151  undom  7198  xpdom3  7208  domunsncan  7210  omxpenlem  7211  disjenex  7267  domssex2  7269  domssex  7270  xpf1o  7271  mapdom3  7281  findcard  7349  fiin  7429  marypha1lem  7440  marypha1  7441  fisupcl  7474  ordiso2  7486  ordtypelem2  7490  ordtypelem6  7494  ordtypelem7  7495  ordtypelem8  7496  wemapso2  7523  brwdom2  7543  unxpwdom2  7558  noinfepOLD  7617  cantnflt  7629  oemapvali  7642  cantnflem1d  7646  wemapwe  7656  cnfcom  7659  rankr1id  7790  tcrank  7810  cardmin2  7887  infxpenlem  7897  infxpenc2lem2  7903  fseqen  7910  dfac8clem  7915  ween  7918  ac5num  7919  indcardi  7924  acni  7928  acni2  7929  acnlem  7931  fodomfi2  7943  infpwfien  7945  inffien  7946  finnisoeu  7996  iunfictbso  7997  acacni  8022  dfac12lem2  8026  infpss  8099  infmap2  8100  ackbij1lem18  8119  ackbij1b  8121  fictb  8127  cfslb2n  8150  cofsmo  8151  cfsmolem  8152  coftr  8155  fin1ai  8175  fin2i  8177  infpssrlem4  8188  domfin4  8193  fin2i2  8200  isfin2-2  8201  fincssdom  8205  ssfin3ds  8212  fin23lem20  8219  fin23lem30  8224  isf32lem3  8237  fin1a2lem12  8293  fin1a2lem13  8294  hsmexlem2  8309  hsmexlem4  8311  axdc2lem  8330  axdc4lem  8337  ac6num  8361  ttukeylem6  8396  axdclem2  8402  imadomg  8414  iundom2g  8417  iundomg  8418  iundom  8419  unirnfdomd  8444  konigthlem  8445  iunctb  8451  fpwwe2  8520  canth4  8524  canthwelem  8527  pwfseqlem3  8537  pwfseqlem5  8540  winalim2  8573  wununi  8583  wunpw  8584  wunelss  8585  r1wunlim  8614  wunex2  8615  tsksdom  8633  tskinf  8646  inttsk  8651  inar1  8652  tskcard  8658  tskurn  8666  gruina  8695  grur1a  8696  grur1  8697  lemul12a  9870  lemulge11  9874  lediv12a  9905  nngt0  10031  peano5uzi  10360  nn0ind-raph  10372  zsupss  10567  suprzub  10569  uzsupss  10570  uzwo3  10571  rpge0  10626  fldiv  11243  uzrdgsuci  11302  fzennn  11309  uzindi  11322  seqcl2  11343  seqcl  11345  seqf  11346  seqfveq2  11347  seqfveq  11349  seqshft2  11351  monoord  11355  monoord2  11356  sermono  11357  seqsplit  11358  seqcaopr3  11360  seqid  11370  seqid2  11371  seqhomo  11372  seqz  11373  expcl2lem  11395  leexp1a  11440  modexp  11516  discr1  11517  discr  11518  faclbnd  11583  faclbnd6  11592  facavg  11594  hashginv  11624  hashf1rn  11638  hashbclem  11703  fz1isolem  11712  seqcoll  11714  s2f1o  11865  f1oun2prg  11866  resqrex  12058  cau3lem  12160  limsupgre  12277  climi  12306  rlimi  12309  rlimclim  12342  climrlim2  12343  rlimcld2  12374  rlimcn1  12384  climcn1  12387  climcn2  12388  isercoll  12463  isercoll2  12464  climsup  12465  caucvgrlem  12468  caurcvgr  12469  iseraltlem2  12478  iseraltlem3  12479  sumeq2ii  12489  summolem3  12510  fsum  12516  fsumadd  12534  fsumm1  12539  fsum1p  12541  fsum2dlem  12556  fsumcom2  12560  fsum0diag2  12568  fsummulc2  12569  fsumge1  12578  fsumabs  12582  fsumtscopo  12583  fsumtscopo2  12584  fsumparts  12587  fsumrelem  12588  fsumrlim  12592  fsumo1  12593  o1fsum  12594  fsumiun  12602  qshash  12608  isum1p  12623  isumrpcl  12625  climcndslem1  12631  climcndslem2  12632  climcnds  12633  cvgrat  12662  mertenslem1  12663  mertens  12665  sin01gt0  12793  sin02gt0  12795  efieq1re  12802  divalglem9  12923  smupvallem  12997  rppwr  13059  algfx  13073  eucalgcvga  13079  prmind2  13092  qredeq  13108  pythagtriplem4  13195  pythagtriplem6  13197  pythagtriplem7  13198  pythagtriplem12  13202  pythagtriplem13  13203  pythagtriplem14  13204  pythagtriplem16  13206  pcmpt  13263  pcmpt2  13264  prmpwdvds  13274  prmreclem2  13287  prmreclem4  13289  prmreclem5  13290  4sqlem11  13325  vdwlem1  13351  vdwlem2  13352  vdwlem9  13359  vdwlem10  13360  vdwlem11  13361  vdwlem12  13362  rami  13385  0ram  13390  0ram2  13391  0ramcl  13393  ramcl  13399  prmlem1  13432  prmlem2  13444  strfvd  13500  strfv2d  13501  strssd  13505  firest  13662  prdsdsval3  13709  imasbas  13740  imasds  13741  imasaddfnlem  13755  imasaddvallem  13756  imasvscafn  13764  divsaddvallem  13778  divsaddflem  13779  divsaddval  13780  divsaddf  13781  divsmulval  13782  divsmulf  13783  isacs1i  13884  mreacs  13885  catidex  13901  catideu  13902  iscatd2  13908  catlid  13910  catrid  13911  subcidcl  14043  funcid  14069  invfuc  14173  yonedalem4c  14376  yonffthlem  14381  mod2ile  14537  lubss  14550  acsmapd  14606  gsumval2a  14784  grpidd2  14844  mulgnegnn  14902  mulgsubcl  14906  divsgrp2  14938  issubg4  14963  ghmf1  15036  pgpssslw  15250  sylow2alem2  15254  fislw  15261  efgsdmi  15366  efgsrel  15368  efgsres  15372  gexexlem  15469  gsumval3  15516  gsumzaddlem  15528  gsummhm2  15537  gsum2d  15548  dprdcntz  15568  dprddisj  15569  dprdss  15589  dprd2dlem2  15600  dprd2da  15602  dpjrid  15622  ablfac1eu  15633  pgpfac1lem1  15634  ablfac2  15649  rngi  15678  divsrng2  15728  issrngd  15951  lssintcl  16042  islbs2  16228  lbsextlem3  16234  lbsextlem4  16235  mplsubglem  16500  mpllsslem  16501  subrgasclcl  16561  zlpirlem3  16772  eltg3  17029  cctop  17072  subbascn  17320  iscncl  17335  cnss2  17343  cnrmi  17426  cmpcov  17454  cmpcovf  17456  fiuncmp  17469  2ndcctbss  17520  2ndcomap  17523  2ndcsep  17524  1stcelcls  17526  islly2  17549  ptpjpre1  17605  elptr  17607  ptbasfi  17615  ptpjopn  17646  ptclsg  17649  dfac14  17652  txcnp  17654  ptcnplem  17655  uptx  17659  txtube  17674  tx2ndc  17685  xkococnlem  17693  cnmpt11  17697  cnmpt21  17705  cnmptkp  17714  cnmptk1p  17719  elqtop  17731  qtoprest  17751  qtopomap  17752  qtopcmap  17753  indishmph  17832  ptcmpfi  17847  kqhmph  17853  csdfil  17928  filssufilg  17945  ufilen  17964  rnelfm  17987  fmfnfmlem4  17991  flimcf  18016  fclscf  18059  alexsubALTlem4  18083  ptcmplem3  18087  ptcmplem4  18088  cnextfvval  18098  cnextcn  18100  tmdgsum2  18128  tsmsxplem2  18185  ucnima  18313  ucncn  18317  imasdsf1olem  18405  imasf1oxmet  18407  metss  18540  comet  18545  met2ndci  18554  prdsxmslem2  18561  metustOLD  18599  metust  18600  cfilucfilOLD  18601  cfilucfil  18602  metutopOLD  18614  psmetutop  18615  opnreen  18864  rectbntr0  18865  fsumcn  18902  rescncf  18929  xrhmeo  18973  cnheiborlem  18981  cnheibor  18982  cnllycmp  18983  lebnumlem1  18988  lebnumlem3  18990  ipcau2  19193  tchcphlem1  19194  tchcphlem2  19195  lmmcvg  19216  cfilss  19225  iscmet3lem1  19246  iscmet3lem2  19247  pjthlem1  19340  pjthlem2  19341  ivthlem1  19350  ivthlem2  19351  ivthlem3  19352  ivth2  19354  ivthle  19355  ivthle2  19356  ivthicc  19357  ovolsslem  19382  ovoliunlem1  19400  ovoliunlem2  19401  ovoliunnul  19405  ovolshftlem1  19407  ovolscalem1  19411  ovolicc2lem3  19417  ovolicc2lem4  19418  voliunlem3  19448  volsup  19452  uniiccdif  19472  uniioombllem2  19477  dyadmbl  19494  volivth  19501  vitalilem3  19504  ismbf3d  19548  mbfimaopnlem  19549  cncombf  19552  mbflimsup  19560  i1fd  19575  itg1addlem4  19593  itg2addlem  19652  itg2gt0  19654  iblitg  19662  itgconst  19712  itgfsum  19720  limcvallem  19760  cnlimci  19778  cnmptlimc  19779  limciun  19783  dvadd  19828  dvmul  19829  dvco  19835  dvrec  19843  dvcnv  19863  dvferm1lem  19870  dvferm1  19871  dvferm2lem  19872  dvferm2  19873  dvferm  19874  rollelem  19875  dvlip  19879  dvlipcn  19880  dvlip2  19881  c1liplem1  19882  c1lip2  19884  dvgt0lem1  19888  dvle  19893  dvivthlem1  19894  lhop1lem  19899  dvcnvrelem1  19903  dvcnvrelem2  19904  dvcvx  19906  dvfsumle  19907  dvfsumge  19908  dvfsumabs  19909  dvfsumlem1  19912  dvfsumlem2  19913  dvfsumlem3  19914  dvfsumlem4  19915  dvfsumrlim2  19918  dvfsum2  19920  ftc1cn  19929  ftc2ditglem  19931  itgsubstlem  19934  evlslem3  19937  evlseu  19939  mpfpf1  19973  pf1mpf  19974  tdeglem4  19985  mdegaddle  19999  mdegmullem  20003  deg1sublt  20035  ply1divmo  20060  fta1g  20092  dgrub  20155  dgradd2  20188  dvply1  20203  plydivex  20216  plyrem  20224  vieta1lem2  20230  aalioulem4  20254  aalioulem5  20255  aalioulem6  20256  aaliou2  20259  taylf  20279  tayl0  20280  ulmi  20304  ulmdvlem1  20318  ulmdvlem3  20320  ulmdv  20321  mtest  20322  pserulm  20340  psercn2  20341  abelth  20359  abelth2  20360  reeff1olem  20364  efif1olem4  20449  efopn  20551  logreclem  20662  isosctrlem2  20665  rlimcnp  20806  rlimcnp2  20807  xrlimcnp  20809  scvxcvx  20826  wilthlem2  20854  basellem4  20868  ppiwordi  20947  fsumdvdscom  20972  musum  20978  musumsum  20979  chtub  20998  fsumvma  20999  chpub  21006  dchrelbas3  21024  dchrelbasd  21025  dchrn0  21036  dchrptlem2  21051  lgsval2lem  21092  lgsdirnn0  21125  lgsdinn0  21126  2sqlem6  21155  2sqlem10  21160  dchrisumlema  21184  dchrisumlem1  21185  dchrisumlem2  21186  dchrisumlem3  21187  dchrmusum2  21190  dchrvmasumlem2  21194  dchrvmasumlem3  21195  dchrvmasumiflem1  21197  dchrisum0flblem2  21205  dchrisum0flb  21206  dchrisum0re  21209  dchrisum0lem1b  21211  dchrisum0lem2  21214  2vmadivsumlem  21236  chpdifbndlem1  21249  selberg3lem1  21253  selberg4lem1  21256  pntrsumbnd2  21263  pntrlog2bndlem2  21274  pntrlog2bndlem3  21275  pntrlog2bndlem5  21277  pntrlog2bndlem6  21279  pntibndlem2  21287  pntibndlem3  21288  pntlemn  21296  pntlemj  21299  pntlemi  21300  pntlemo  21303  pntlem3  21305  pntlemp  21306  pntleml  21307  ostth2lem1  21314  ostth2lem2  21330  ostth3  21334  usgraedgleord  21415  nbgrassovt  21449  nbgraf1o0  21458  cusgraexg  21480  cusgrafilem2  21491  cusgrafilem3  21492  sizeusglecusg  21497  1conngra  21664  vdusgraval  21680  isgrp2d  21825  opidon  21912  ghgrp  21958  rngodm1dm2  22008  zerdivemp1  22024  ubthlem1  22374  ubthlem2  22375  minvecolem3  22380  minvecolem4b  22382  minvecolem4  22384  bcsiALT  22683  occllem  22807  pjhthlem1  22895  ococin  22912  spanpr  23084  pjorthi  23173  nmbdoplbi  23529  nmcoplbi  23533  nmbdfnlbi  23554  nmcfnlbi  23557  nmopcoi  23600  branmfn  23610  hstnmoc  23728  mdsl0  23815  atomli  23887  atcvat4i  23902  atabsi  23906  abrexdomjm  23990  elpreq  24001  ifeqeqx  24003  fovcld  24052  fnct  24107  xlt2addrd  24126  supxrnemnf  24129  ssnnssfz  24150  resspos  24189  resstos  24190  ofldsqr  24242  fmcncfil  24319  xrge0iifiso  24323  elzdif0  24366  qqhval2lem  24367  esumcst  24457  esumpinfval  24465  esumpinfsum  24469  sigaclci  24517  insiga  24522  measres  24578  measdivcstOLD  24580  mbfmcnvima  24609  dya2iocnrect  24633  dya2iocnei  24634  ballotlemfp1  24751  ballotlemfrcn0  24789  lgamgulmlem5  24819  lgamcvglem  24826  derangenlem  24859  subfacp1lem3  24870  subfacp1lem5  24872  rescon  24935  cvmliftlem3  24976  cvmlift2lem10  25001  relexpadd  25140  relexpindlem  25141  rtrclreclem.trans  25148  dedekind  25189  ntrivcvgn0  25228  prodeq2ii  25241  prodmolem3  25261  fprod  25269  fprodmul  25286  fproddiv  25287  fprodm1  25292  fprod1p  25293  fprod2dlem  25306  fprodcom2  25310  wfrlem4  25543  wfrlem15  25554  frrlem4  25587  sltres  25621  nobndlem2  25650  nobndup  25657  nobnddown  25658  nofulllem3  25661  nofulllem5  25663  axlowdimlem16  25898  axlowdimlem17  25899  axcontlem3  25907  axcontlem10  25914  cgrextend  25944  segconeq  25946  trisegint  25964  ontgval  26183  wl-bitrd  26224  ftc1cnnclem  26280  ftc1cnnc  26281  ftc2nc  26291  ivthALT  26340  fnessref  26375  refssfne  26376  comppfsc  26389  neibastop1  26390  filnetlem4  26412  abrexdom  26434  indexdom  26438  mettrifi  26465  equivtotbnd  26489  totbndbnd  26500  prdstotbnd  26505  heibor1lem  26520  bfplem1  26533  bfplem2  26534  zerdivemp1x  26573  ofmpteq  26778  mzpsubmpt  26802  mzpsubst  26807  eqrabdioph  26838  rabdiophlem2  26864  elpell14qr2  26927  elpell1qr2  26937  pellfundre  26946  pellfundge  26947  pellfundglb  26950  pellfund14gap  26952  congabseq  27041  dvdsleabs2  27057  jm2.22  27068  jm2.23  27069  jm2.26lem3  27074  wepwsolem  27118  dnwech  27125  aomclem2  27132  aomclem4  27134  frlmup4  27232  lindff1  27269  lindfrn  27270  lmisfree  27291  dgrnznn  27319  psgnunilem4  27399  sbiota1  27613  refsumcn  27679  rfcnnnub  27685  fmul01  27688  fmuldfeqlem1  27690  fmuldfeq  27691  fmul01lt1lem1  27692  fmul01lt1lem2  27693  cncfmptss  27695  climinf  27710  climsuselem1  27711  climsuse  27712  stoweidlem3  27730  stoweidlem16  27743  stoweidlem17  27744  stoweidlem19  27746  stoweidlem20  27747  stoweidlem23  27750  stoweidlem25  27752  stoweidlem27  27754  stoweidlem31  27758  stoweidlem34  27761  stoweidlem42  27769  stoweidlem48  27775  stoweidlem51  27778  stoweidlem52  27779  stoweidlem59  27786  wallispilem1  27792  wallispilem3  27794  stirlinglem13  27813  2leaddle2  28103  fz0fzelfz0  28129  fz0fzdiffz0  28130  flltdivnn0lt  28158  hashimarn  28174  wrdsymb0  28190  ccatsymb  28199  swrdvalodm2  28210  swrdvalodm  28211  swrd0swrdid  28222  swrdswrd0  28223  swrd0swrd0  28224  swrdccatin12  28236  swrdccat3  28237  swrdccat  28238  modprm0  28250  cshwoor  28259  cshwidx  28264  cshwidxmod  28265  cshwidxm1  28267  cshwidxm  28268  cshwidxn  28269  2cshw1lem1  28270  2cshw1lem2  28271  2cshw2lem1  28274  2cshw2lem2  28275  lswrd0  28283  cshweqrep  28296  cshwssizelem1a  28301  cshwssizelem2  28303  cshwssizelem4a  28305  nbgrassvwo  28317  usgra2wlkspth  28334  usgra2pthlem1  28336  usgra2adedgwlk  28342  usgra2adedgwlkon  28343  wlkiswwlk2lem3  28363  frgranbnb  28472  frgrancvvdeqlem3  28483  frgrancvvdeqlem9  28492  frg2woteu  28506  frg2woteqm  28510  usgreghash2spotv  28517  ordelordALT  28684  2pm13.193  28701  ee11an  28853  eel2221  28866  bnj1379  29264  bnj580  29346  bnj944  29371  bnj999  29390  bnj1204  29443  bnj1398  29465  omllaw5N  30107  cmtcomlemN  30108  cmtbr3N  30114  omlfh3N  30119  atlen0  30170  exatleN  30263  hlrelat3  30271  cvrexchlem  30278  atlelt  30297  cvrat4  30302  4atlem11b  30467  4atlem12b  30470  lneq2at  30637  cdlema1N  30650  cdlemblem  30652  paddss12  30678  paddasslem2  30680  paddasslem4  30682  paddasslem6  30684  paddasslem12  30690  paddunN  30786  poml4N  30812  poml5N  30813  osumcllem6N  30820  pexmidlem6N  30834  pl42lem2N  30839  ltrnu  30980  ltrneq2  31007  trlval2  31022  cdlemd6  31062  cdleme25b  31213  cdleme29b  31234  cdlemefr29exN  31261  ltrniotacnvval  31441  cdlemk28-3  31767  dochexmidlem7  32326
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator