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  2234  equid1  2236  elex22  2968  elex2  2969  spcimdv  3034  spsbcd  3175  disjxiun  4210  opth  4436  euotd  4458  wereu  4579  wereu2  4580  tz7.7  4608  reusv2lem3  4727  ssorduni  4767  suceloni  4794  nlimsucg  4823  tfisi  4839  unielrel  5395  funmo  5471  iinpreima  5861  zfrep6  5969  fnfvima  5977  fliftfun  6035  fliftval  6039  weniso  6076  knatar  6081  grprinvlem  6286  grprinvd  6287  caofref  6331  curry1  6439  curry2  6442  fnwelem  6462  riota5f  6575  riotass2  6578  smogt  6630  omeulem1  6826  oeworde  6837  oelimcl  6844  oeeulem  6845  oeeui  6846  nnawordex  6881  oaabs2  6889  ertr  6921  swoso  6937  qliftlem  6986  th3q  7014  resixp  7098  f1dom2g  7126  dom3d  7150  undom  7197  xpdom3  7207  domunsncan  7209  omxpenlem  7210  disjenex  7266  domssex2  7268  domssex  7269  xpf1o  7270  mapdom3  7280  findcard  7348  fiin  7428  marypha1lem  7439  marypha1  7440  fisupcl  7473  ordiso2  7485  ordtypelem2  7489  ordtypelem6  7493  ordtypelem7  7494  ordtypelem8  7495  wemapso2  7522  brwdom2  7542  unxpwdom2  7557  noinfepOLD  7616  cantnflt  7628  oemapvali  7641  cantnflem1d  7645  wemapwe  7655  cnfcom  7658  rankr1id  7789  tcrank  7809  cardmin2  7886  infxpenlem  7896  infxpenc2lem2  7902  fseqen  7909  dfac8clem  7914  ween  7917  ac5num  7918  indcardi  7923  acni  7927  acni2  7928  acnlem  7930  fodomfi2  7942  infpwfien  7944  inffien  7945  finnisoeu  7995  iunfictbso  7996  acacni  8021  dfac12lem2  8025  infpss  8098  infmap2  8099  ackbij1lem18  8118  ackbij1b  8120  fictb  8126  cfslb2n  8149  cofsmo  8150  cfsmolem  8151  coftr  8154  fin1ai  8174  fin2i  8176  infpssrlem4  8187  domfin4  8192  fin2i2  8199  isfin2-2  8200  fincssdom  8204  ssfin3ds  8211  fin23lem20  8218  fin23lem30  8223  isf32lem3  8236  fin1a2lem12  8292  fin1a2lem13  8293  hsmexlem2  8308  hsmexlem4  8310  axdc2lem  8329  axdc4lem  8336  ac6num  8360  ttukeylem6  8395  axdclem2  8401  imadomg  8413  iundom2g  8416  iundomg  8417  iundom  8418  unirnfdomd  8443  konigthlem  8444  iunctb  8450  fpwwe2  8519  canth4  8523  canthwelem  8526  pwfseqlem3  8536  pwfseqlem5  8539  winalim2  8572  wununi  8582  wunpw  8583  wunelss  8584  r1wunlim  8613  wunex2  8614  tsksdom  8632  tskinf  8645  inttsk  8650  inar1  8651  tskcard  8657  tskurn  8665  gruina  8694  grur1a  8695  grur1  8696  lemul12a  9869  lemulge11  9873  lediv12a  9904  nngt0  10030  peano5uzi  10359  nn0ind-raph  10371  zsupss  10566  suprzub  10568  uzsupss  10569  uzwo3  10570  rpge0  10625  fldiv  11242  uzrdgsuci  11301  fzennn  11308  uzindi  11321  seqcl2  11342  seqcl  11344  seqf  11345  seqfveq2  11346  seqfveq  11348  seqshft2  11350  monoord  11354  monoord2  11355  sermono  11356  seqsplit  11357  seqcaopr3  11359  seqid  11369  seqid2  11370  seqhomo  11371  seqz  11372  expcl2lem  11394  leexp1a  11439  modexp  11515  discr1  11516  discr  11517  faclbnd  11582  faclbnd6  11591  facavg  11593  hashginv  11623  hashf1rn  11637  hashbclem  11702  fz1isolem  11711  seqcoll  11713  s2f1o  11864  f1oun2prg  11865  resqrex  12057  cau3lem  12159  limsupgre  12276  climi  12305  rlimi  12308  rlimclim  12341  climrlim2  12342  rlimcld2  12373  rlimcn1  12383  climcn1  12386  climcn2  12387  isercoll  12462  isercoll2  12463  climsup  12464  caucvgrlem  12467  caurcvgr  12468  iseraltlem2  12477  iseraltlem3  12478  sumeq2ii  12488  summolem3  12509  fsum  12515  fsumadd  12533  fsumm1  12538  fsum1p  12540  fsum2dlem  12555  fsumcom2  12559  fsum0diag2  12567  fsummulc2  12568  fsumge1  12577  fsumabs  12581  fsumtscopo  12582  fsumtscopo2  12583  fsumparts  12586  fsumrelem  12587  fsumrlim  12591  fsumo1  12592  o1fsum  12593  fsumiun  12601  qshash  12607  isum1p  12622  isumrpcl  12624  climcndslem1  12630  climcndslem2  12631  climcnds  12632  cvgrat  12661  mertenslem1  12662  mertens  12664  sin01gt0  12792  sin02gt0  12794  efieq1re  12801  divalglem9  12922  smupvallem  12996  rppwr  13058  algfx  13072  eucalgcvga  13078  prmind2  13091  qredeq  13107  pythagtriplem4  13194  pythagtriplem6  13196  pythagtriplem7  13197  pythagtriplem12  13201  pythagtriplem13  13202  pythagtriplem14  13203  pythagtriplem16  13205  pcmpt  13262  pcmpt2  13263  prmpwdvds  13273  prmreclem2  13286  prmreclem4  13288  prmreclem5  13289  4sqlem11  13324  vdwlem1  13350  vdwlem2  13351  vdwlem9  13358  vdwlem10  13359  vdwlem11  13360  vdwlem12  13361  rami  13384  0ram  13389  0ram2  13390  0ramcl  13392  ramcl  13398  prmlem1  13431  prmlem2  13443  strfvd  13499  strfv2d  13500  strssd  13504  firest  13661  prdsdsval3  13708  imasbas  13739  imasds  13740  imasaddfnlem  13754  imasaddvallem  13755  imasvscafn  13763  divsaddvallem  13777  divsaddflem  13778  divsaddval  13779  divsaddf  13780  divsmulval  13781  divsmulf  13782  isacs1i  13883  mreacs  13884  catidex  13900  catideu  13901  iscatd2  13907  catlid  13909  catrid  13910  subcidcl  14042  funcid  14068  invfuc  14172  yonedalem4c  14375  yonffthlem  14380  mod2ile  14536  lubss  14549  acsmapd  14605  gsumval2a  14783  grpidd2  14843  mulgnegnn  14901  mulgsubcl  14905  divsgrp2  14937  issubg4  14962  ghmf1  15035  pgpssslw  15249  sylow2alem2  15253  fislw  15260  efgsdmi  15365  efgsrel  15367  efgsres  15371  gexexlem  15468  gsumval3  15515  gsumzaddlem  15527  gsummhm2  15536  gsum2d  15547  dprdcntz  15567  dprddisj  15568  dprdss  15588  dprd2dlem2  15599  dprd2da  15601  dpjrid  15621  ablfac1eu  15632  pgpfac1lem1  15633  ablfac2  15648  rngi  15677  divsrng2  15727  issrngd  15950  lssintcl  16041  islbs2  16227  lbsextlem3  16233  lbsextlem4  16234  mplsubglem  16499  mpllsslem  16500  subrgasclcl  16560  zlpirlem3  16771  eltg3  17028  cctop  17071  subbascn  17319  iscncl  17334  cnss2  17342  cnrmi  17425  cmpcov  17453  cmpcovf  17455  fiuncmp  17468  2ndcctbss  17519  2ndcomap  17522  2ndcsep  17523  1stcelcls  17525  islly2  17548  ptpjpre1  17604  elptr  17606  ptbasfi  17614  ptpjopn  17645  ptclsg  17648  dfac14  17651  txcnp  17653  ptcnplem  17654  uptx  17658  txtube  17673  tx2ndc  17684  xkococnlem  17692  cnmpt11  17696  cnmpt21  17704  cnmptkp  17713  cnmptk1p  17718  elqtop  17730  qtoprest  17750  qtopomap  17751  qtopcmap  17752  indishmph  17831  ptcmpfi  17846  kqhmph  17852  csdfil  17927  filssufilg  17944  ufilen  17963  rnelfm  17986  fmfnfmlem4  17990  flimcf  18015  fclscf  18058  alexsubALTlem4  18082  ptcmplem3  18086  ptcmplem4  18087  cnextfvval  18097  cnextcn  18099  tmdgsum2  18127  tsmsxplem2  18184  ucnima  18312  ucncn  18316  imasdsf1olem  18404  imasf1oxmet  18406  metss  18539  comet  18544  met2ndci  18553  prdsxmslem2  18560  metustOLD  18598  metust  18599  cfilucfilOLD  18600  cfilucfil  18601  metutopOLD  18613  psmetutop  18614  opnreen  18863  rectbntr0  18864  fsumcn  18901  rescncf  18928  xrhmeo  18972  cnheiborlem  18980  cnheibor  18981  cnllycmp  18982  lebnumlem1  18987  lebnumlem3  18989  ipcau2  19192  tchcphlem1  19193  tchcphlem2  19194  lmmcvg  19215  cfilss  19224  iscmet3lem1  19245  iscmet3lem2  19246  pjthlem1  19339  pjthlem2  19340  ivthlem1  19349  ivthlem2  19350  ivthlem3  19351  ivth2  19353  ivthle  19354  ivthle2  19355  ivthicc  19356  ovolsslem  19381  ovoliunlem1  19399  ovoliunlem2  19400  ovoliunnul  19404  ovolshftlem1  19406  ovolscalem1  19410  ovolicc2lem3  19416  ovolicc2lem4  19417  voliunlem3  19447  volsup  19451  uniiccdif  19471  uniioombllem2  19476  dyadmbl  19493  volivth  19500  vitalilem3  19503  ismbf3d  19547  mbfimaopnlem  19548  cncombf  19551  mbflimsup  19559  i1fd  19574  itg1addlem4  19592  itg2addlem  19651  itg2gt0  19653  iblitg  19661  itgconst  19711  itgfsum  19719  limcvallem  19759  cnlimci  19777  cnmptlimc  19778  limciun  19782  dvadd  19827  dvmul  19828  dvco  19834  dvrec  19842  dvcnv  19862  dvferm1lem  19869  dvferm1  19870  dvferm2lem  19871  dvferm2  19872  dvferm  19873  rollelem  19874  dvlip  19878  dvlipcn  19879  dvlip2  19880  c1liplem1  19881  c1lip2  19883  dvgt0lem1  19887  dvle  19892  dvivthlem1  19893  lhop1lem  19898  dvcnvrelem1  19902  dvcnvrelem2  19903  dvcvx  19905  dvfsumle  19906  dvfsumge  19907  dvfsumabs  19908  dvfsumlem1  19911  dvfsumlem2  19912  dvfsumlem3  19913  dvfsumlem4  19914  dvfsumrlim2  19917  dvfsum2  19919  ftc1cn  19928  ftc2ditglem  19930  itgsubstlem  19933  evlslem3  19936  evlseu  19938  mpfpf1  19972  pf1mpf  19973  tdeglem4  19984  mdegaddle  19998  mdegmullem  20002  deg1sublt  20034  ply1divmo  20059  fta1g  20091  dgrub  20154  dgradd2  20187  dvply1  20202  plydivex  20215  plyrem  20223  vieta1lem2  20229  aalioulem4  20253  aalioulem5  20254  aalioulem6  20255  aaliou2  20258  taylf  20278  tayl0  20279  ulmi  20303  ulmdvlem1  20317  ulmdvlem3  20319  ulmdv  20320  mtest  20321  pserulm  20339  psercn2  20340  abelth  20358  abelth2  20359  reeff1olem  20363  efif1olem4  20448  efopn  20550  logreclem  20661  isosctrlem2  20664  rlimcnp  20805  rlimcnp2  20806  xrlimcnp  20808  scvxcvx  20825  wilthlem2  20853  basellem4  20867  ppiwordi  20946  fsumdvdscom  20971  musum  20977  musumsum  20978  chtub  20997  fsumvma  20998  chpub  21005  dchrelbas3  21023  dchrelbasd  21024  dchrn0  21035  dchrptlem2  21050  lgsval2lem  21091  lgsdirnn0  21124  lgsdinn0  21125  2sqlem6  21154  2sqlem10  21159  dchrisumlema  21183  dchrisumlem1  21184  dchrisumlem2  21185  dchrisumlem3  21186  dchrmusum2  21189  dchrvmasumlem2  21193  dchrvmasumlem3  21194  dchrvmasumiflem1  21196  dchrisum0flblem2  21204  dchrisum0flb  21205  dchrisum0re  21208  dchrisum0lem1b  21210  dchrisum0lem2  21213  2vmadivsumlem  21235  chpdifbndlem1  21248  selberg3lem1  21252  selberg4lem1  21255  pntrsumbnd2  21262  pntrlog2bndlem2  21273  pntrlog2bndlem3  21274  pntrlog2bndlem5  21276  pntrlog2bndlem6  21278  pntibndlem2  21286  pntibndlem3  21287  pntlemn  21295  pntlemj  21298  pntlemi  21299  pntlemo  21302  pntlem3  21304  pntlemp  21305  pntleml  21306  ostth2lem1  21313  ostth2lem2  21329  ostth3  21333  usgraedgleord  21414  nbgrassovt  21448  nbgraf1o0  21457  cusgraexg  21479  cusgrafilem2  21490  cusgrafilem3  21491  sizeusglecusg  21496  1conngra  21663  vdusgraval  21679  isgrp2d  21824  opidon  21911  ghgrp  21957  rngodm1dm2  22007  zerdivemp1  22023  ubthlem1  22373  ubthlem2  22374  minvecolem3  22379  minvecolem4b  22381  minvecolem4  22383  bcsiALT  22682  occllem  22806  pjhthlem1  22894  ococin  22911  spanpr  23083  pjorthi  23172  nmbdoplbi  23528  nmcoplbi  23532  nmbdfnlbi  23553  nmcfnlbi  23556  nmopcoi  23599  branmfn  23609  hstnmoc  23727  mdsl0  23814  atomli  23886  atcvat4i  23901  atabsi  23905  abrexdomjm  23989  elpreq  24000  ifeqeqx  24002  fovcld  24051  fnct  24106  xlt2addrd  24125  supxrnemnf  24128  ssnnssfz  24149  resspos  24188  resstos  24189  ofldsqr  24241  fmcncfil  24318  xrge0iifiso  24322  elzdif0  24365  qqhval2lem  24366  esumcst  24456  esumpinfval  24464  esumpinfsum  24468  sigaclci  24516  insiga  24521  measres  24577  measdivcstOLD  24579  mbfmcnvima  24608  dya2iocnrect  24632  dya2iocnei  24633  ballotlemfp1  24750  ballotlemfrcn0  24788  lgamgulmlem5  24818  lgamcvglem  24825  derangenlem  24858  subfacp1lem3  24869  subfacp1lem5  24871  rescon  24934  cvmliftlem3  24975  cvmlift2lem10  25000  relexpadd  25139  relexpindlem  25140  rtrclreclem.trans  25147  dedekind  25188  ntrivcvgn0  25227  prodeq2ii  25240  prodmolem3  25260  fprod  25268  fprodmul  25285  fproddiv  25286  fprodm1  25291  fprod1p  25292  fprod2dlem  25305  fprodcom2  25309  wfrlem4  25542  wfrlem15  25553  frrlem4  25586  sltres  25620  nobndlem2  25649  nobndup  25656  nobnddown  25657  nofulllem3  25660  nofulllem5  25662  axlowdimlem16  25897  axlowdimlem17  25898  axcontlem3  25906  axcontlem10  25913  cgrextend  25943  segconeq  25945  trisegint  25963  ontgval  26182  wl-bitrd  26223  ftc1cnnclem  26279  ftc1cnnc  26280  ftc2nc  26290  ivthALT  26339  fnessref  26374  refssfne  26375  comppfsc  26388  neibastop1  26389  filnetlem4  26411  abrexdom  26433  indexdom  26437  mettrifi  26464  equivtotbnd  26488  totbndbnd  26499  prdstotbnd  26504  heibor1lem  26519  bfplem1  26532  bfplem2  26533  zerdivemp1x  26572  ofmpteq  26777  mzpsubmpt  26801  mzpsubst  26806  eqrabdioph  26837  rabdiophlem2  26863  elpell14qr2  26926  elpell1qr2  26936  pellfundre  26945  pellfundge  26946  pellfundglb  26949  pellfund14gap  26951  congabseq  27040  dvdsleabs2  27056  jm2.22  27067  jm2.23  27068  jm2.26lem3  27073  wepwsolem  27117  dnwech  27124  aomclem2  27131  aomclem4  27133  frlmup4  27231  lindff1  27268  lindfrn  27269  lmisfree  27290  dgrnznn  27318  psgnunilem4  27398  sbiota1  27612  refsumcn  27678  rfcnnnub  27684  fmul01  27687  fmuldfeqlem1  27689  fmuldfeq  27690  fmul01lt1lem1  27691  fmul01lt1lem2  27692  cncfmptss  27694  climinf  27709  climsuselem1  27710  climsuse  27711  stoweidlem3  27729  stoweidlem16  27742  stoweidlem17  27743  stoweidlem19  27745  stoweidlem20  27746  stoweidlem23  27749  stoweidlem25  27751  stoweidlem27  27753  stoweidlem31  27757  stoweidlem34  27760  stoweidlem42  27768  stoweidlem48  27774  stoweidlem51  27777  stoweidlem52  27778  stoweidlem59  27785  wallispilem1  27791  wallispilem3  27793  stirlinglem13  27812  2leaddle2  28093  fz0fzelfz0  28119  fz0fzdiffz0  28120  flltdivnn0lt  28148  hashimarn  28164  wrdsymb0  28171  ccatsymb  28180  swrdvalodm2  28189  swrdvalodm  28190  swrd0swrdid  28201  swrdswrd0  28202  swrd0swrd0  28203  swrdccatin12  28215  swrdccat3  28216  swrdccat  28217  modprm0  28229  cshwoor  28238  cshwidx  28243  cshwidxmod  28244  cshwidxm1  28246  cshwidxm  28247  cshwidxn  28248  2cshw1lem1  28249  2cshw1lem2  28250  2cshw2lem1  28253  2cshw2lem2  28254  lswrd0  28262  cshweqrep  28275  cshwssizelem1a  28280  cshwssizelem2  28282  cshwssizelem4a  28284  usgra2wlkspth  28309  usgra2pthlem1  28311  usgra2adedgwlk  28317  usgra2adedgwlkon  28318  frgranbnb  28411  frgrancvvdeqlem3  28422  frgrancvvdeqlem9  28431  frg2woteu  28445  frg2woteqm  28449  usgreghash2spotv  28456  ordelordALT  28623  2pm13.193  28640  ee11an  28792  eel2221  28805  bnj1379  29203  bnj580  29285  bnj944  29310  bnj999  29329  bnj1204  29382  bnj1398  29404  omllaw5N  30046  cmtcomlemN  30047  cmtbr3N  30053  omlfh3N  30058  atlen0  30109  exatleN  30202  hlrelat3  30210  cvrexchlem  30217  atlelt  30236  cvrat4  30241  4atlem11b  30406  4atlem12b  30409  lneq2at  30576  cdlema1N  30589  cdlemblem  30591  paddss12  30617  paddasslem2  30619  paddasslem4  30621  paddasslem6  30623  paddasslem12  30629  paddunN  30725  poml4N  30751  poml5N  30752  osumcllem6N  30759  pexmidlem6N  30773  pl42lem2N  30778  ltrnu  30919  ltrneq2  30946  trlval2  30961  cdlemd6  31001  cdleme25b  31152  cdleme29b  31173  cdlemefr29exN  31200  ltrniotacnvval  31380  cdlemk28-3  31706  dochexmidlem7  32265
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator