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

Theorem sylc 60
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 38 . 2  |-  ( ph  ->  ( ph  ->  th )
)
54pm2.43i 47 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
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  61  mpsyl  63  jc  147  2thd  240  jca  532  syl2anc  661  nfimd  1852  ax13fromc9  2213  equid1  2215  elex2  3080  elex22  3081  spcimdv  3150  spsbcd  3298  disjxiun  4387  reusv2lem3  4593  opth  4664  euotd  4690  wereu  4814  wereu2  4815  tz7.7  4843  unielrel  5460  funmo  5532  iinpreima  5932  fnfvima  6054  fliftfun  6104  fliftval  6108  weniso  6144  knatar  6147  riota5f  6176  riotass2  6178  grprinvlem  6401  grprinvd  6402  ofmpteq  6438  caofref  6446  ssorduni  6497  suceloni  6524  nlimsucg  6553  tfisi  6569  zfrep6  6645  curry1  6764  curry2  6767  fnwelem  6787  funsssuppss  6815  smogt  6928  tfrlem1  6935  tfrlem5  6939  omeulem1  7121  oeworde  7132  oelimcl  7139  oeeulem  7140  oeeui  7141  nnawordex  7176  oaabs2  7184  ertr  7216  swoso  7232  qliftlem  7281  th3q  7309  resixp  7398  f1dom2g  7427  dom3d  7451  undom  7499  xpdom3  7509  domunsncan  7511  omxpenlem  7512  disjenex  7569  domssex2  7571  domssex  7572  xpf1o  7573  mapdom3  7583  findcard  7652  fiin  7773  marypha1lem  7784  marypha1  7785  fisupcl  7818  ordiso2  7830  ordtypelem2  7834  ordtypelem6  7838  ordtypelem7  7839  ordtypelem8  7840  wemapso2OLD  7867  wemapso2lem  7868  brwdom2  7889  unxpwdom2  7904  noinfepOLD  7967  cantnflt  7981  cantnfrescl  7985  oemapvali  7993  cantnflem1d  7997  cantnfltOLD  8011  cantnflem1dOLD  8020  wemapwe  8029  wemapweOLD  8030  cnfcom  8034  cnfcomOLD  8042  rankr1id  8170  tcrank  8192  cardmin2  8269  infxpenlem  8281  infxpenc2lem2  8287  infxpenc2lem2OLD  8291  fseqen  8298  dfac8clem  8303  ween  8306  ac5num  8307  indcardi  8312  acni  8316  acni2  8317  acnlem  8319  fodomfi2  8331  infpwfien  8333  inffien  8334  finnisoeu  8384  iunfictbso  8385  acacni  8410  dfac12lem2  8414  infpss  8487  infmap2  8488  ackbij1lem18  8507  ackbij1b  8509  fictb  8515  cfslb2n  8538  cofsmo  8539  cfsmolem  8540  coftr  8543  fin1ai  8563  fin2i  8565  infpssrlem4  8576  domfin4  8581  fin2i2  8588  isfin2-2  8589  fincssdom  8593  ssfin3ds  8600  fin23lem20  8607  fin23lem30  8612  isf32lem3  8625  fin1a2lem12  8681  fin1a2lem13  8682  hsmexlem2  8697  hsmexlem4  8699  axdc2lem  8718  axdc4lem  8725  ac6num  8749  ttukeylem6  8784  axdclem2  8790  imadomg  8802  iundom2g  8805  iundomg  8806  iundom  8807  unirnfdomd  8832  konigthlem  8833  iunctb  8839  fpwwe2  8911  canth4  8915  canthwelem  8918  pwfseqlem3  8928  pwfseqlem5  8931  winalim2  8964  wununi  8974  wunpw  8975  wunelss  8976  r1wunlim  9005  wunex2  9006  tsksdom  9024  tskinf  9037  inttsk  9042  inar1  9043  tskcard  9049  tskurn  9057  gruina  9086  grur1a  9087  grur1  9088  dedekind  9634  lemul12a  10288  lemulge11  10292  lediv12a  10326  nngt0  10452  peano5uzi  10831  nn0ind-raph  10843  zsupss  11045  suprzub  11047  uzsupss  11048  uzwo3  11049  rpge0  11104  fz0fzelfz0  11587  fz0fzdiffz0  11590  elfzodifsumelfzo  11705  fzonfzoufzol  11729  flltdivnn0lt  11778  fldiv  11800  modaddmodup  11863  uzrdgsuci  11884  fzennn  11891  uzindi  11904  seqcl2  11925  seqcl  11927  seqf  11928  seqfveq2  11929  seqfveq  11931  seqshft2  11933  monoord  11937  monoord2  11938  sermono  11939  seqsplit  11940  seqcaopr3  11942  seqid  11952  seqid2  11953  seqhomo  11954  seqz  11955  expcl2lem  11978  leexp1a  12023  modexp  12100  discr1  12101  discr  12102  faclbnd  12167  faclbnd6  12176  facavg  12178  hashginv  12208  hashf1rn  12224  hashge2el2dif  12286  hashimarn  12302  hashbclem  12307  fz1isolem  12316  seqcoll  12318  wrdsymb0  12361  wrdlenge2n0  12363  lsw0  12369  ccatsymb  12383  swrdvalodm2  12435  swrdvalodm  12436  swrdswrd0  12458  swrd0swrd0  12459  wrd2ind  12474  swrdccatin12  12484  swrdccat3  12485  swrdccat  12486  swrdccatid  12490  swrdccatin1d  12492  swrdccatin12d  12494  repswswrd  12524  cshwidxmod  12542  s2f1o  12628  f1oun2prg  12629  resqrex  12842  cau3lem  12944  limsupgre  13061  climi  13090  rlimi  13093  rlimclim  13126  climrlim2  13127  rlimcld2  13158  rlimcn1  13168  climcn1  13171  climcn2  13172  isercoll  13247  isercoll2  13248  climsup  13249  caucvgrlem  13252  caurcvgr  13253  iseraltlem2  13262  iseraltlem3  13263  sumeq2ii  13272  summolem3  13293  zsum  13297  fsum  13299  fsumadd  13317  fsumm1  13322  fsum1p  13324  fsum2dlem  13339  fsumcom2  13343  fsum0diag2  13352  fsummulc2  13353  fsumge1  13362  fsumabs  13366  fsumtscopo  13367  fsumtscopo2  13368  fsumparts  13371  fsumrelem  13372  fsumrlim  13376  fsumo1  13377  o1fsum  13378  fsumiun  13386  qshash  13392  isum1p  13406  isumrpcl  13408  climcndslem1  13414  climcndslem2  13415  climcnds  13416  cvgrat  13445  mertenslem1  13446  mertens  13448  sin01gt0  13576  sin02gt0  13578  efieq1re  13585  divalglem9  13707  smupvallem  13781  rppwr  13843  algfx  13857  eucalgcvga  13863  prmind2  13876  qredeq  13894  modprm0  13975  pythagtriplem4  13988  pythagtriplem6  13990  pythagtriplem7  13991  pythagtriplem12  13995  pythagtriplem13  13996  pythagtriplem14  13997  pythagtriplem16  13999  pcmpt  14056  pcmpt2  14057  prmpwdvds  14067  prmreclem2  14080  prmreclem4  14082  prmreclem5  14083  4sqlem11  14118  vdwlem1  14144  vdwlem2  14145  vdwlem9  14152  vdwlem10  14153  vdwlem11  14154  vdwlem12  14155  rami  14178  0ram  14183  0ram2  14184  0ramcl  14186  ramcl  14192  cshwsidrepsw  14222  cshwshashlem2  14225  prmlem1  14237  prmlem2  14249  strfvd  14307  strfv2d  14308  strssd  14312  firest  14473  prdsdsval3  14525  imasbas  14552  imasds  14553  imasaddfnlem  14568  imasaddvallem  14569  imasvscafn  14577  divsaddvallem  14591  divsaddflem  14592  divsaddval  14593  divsaddf  14594  divsmulval  14595  divsmulf  14596  isacs1i  14697  mreacs  14698  catidex  14714  catideu  14715  iscatd2  14721  catlid  14723  catrid  14724  subcidcl  14856  funcid  14882  invfuc  14986  yonedalem4c  15189  yonffthlem  15194  mod2ile  15378  lubss  15393  acsmapd  15450  mrcmndind  15596  gsumval2a  15614  grpidd2  15677  mulgnegnn  15739  mulgsubcl  15743  divsgrp2  15775  issubg4  15802  ghmf1  15877  pgrpsubgsymg  16015  fvcosymgeq  16036  gsmsymgreqlem1  16037  psgnunilem4  16105  pgpssslw  16217  sylow2alem2  16221  fislw  16228  efgsdmi  16333  efgsrel  16335  efgsres  16339  gexexlem  16438  gsumval3OLD  16486  gsumval3lem2  16488  gsumzaddlem  16512  gsumzaddlemOLD  16514  gsummhm2  16539  gsummhm2OLD  16540  gsum2d  16568  gsum2dOLD  16569  dprddomcld  16588  dprdcntz  16597  dprddisj  16598  dprdss  16631  dprd2dlem2  16644  dprd2da  16646  dpjrid  16666  ablfac1eu  16679  pgpfac1lem1  16680  ablfac2  16695  srgi  16718  rngi  16763  divsrng2  16818  issrngd  17052  lssintcl  17151  islbs2  17341  lbsextlem3  17347  lbsextlem4  17348  mplsubglem  17617  mpllsslem  17618  mplsubglemOLD  17619  mpllsslemOLD  17620  subrgasclcl  17688  evlslem3  17707  evlseu  17709  mpfpf1  17894  pf1mpf  17895  zringlpirlem3  18014  zlpirlem3  18019  psgnodpm  18127  psgndiflemB  18139  frlmphl  18315  frlmup4  18338  lindff1  18358  lindfrn  18359  lmisfree  18380  mdetdiagid  18522  mdet1  18523  mdetralt  18530  mdetunilem9  18542  slesolinv  18602  cramerimp  18608  eltg3  18683  cctop  18726  subbascn  18974  iscncl  18989  cnss2  18997  cnrmi  19080  cmpcov  19108  cmpcovf  19110  fiuncmp  19123  2ndcctbss  19175  2ndcomap  19178  2ndcsep  19179  1stcelcls  19181  islly2  19204  ptpjpre1  19260  elptr  19262  ptbasfi  19270  ptpjopn  19301  ptclsg  19304  dfac14  19307  txcnp  19309  ptcnplem  19310  uptx  19314  txtube  19329  tx2ndc  19340  xkococnlem  19348  cnmpt11  19352  cnmpt21  19360  cnmptkp  19369  cnmptk1p  19374  elqtop  19386  qtoprest  19406  qtopomap  19407  qtopcmap  19408  indishmph  19487  ptcmpfi  19502  kqhmph  19508  csdfil  19583  filssufilg  19600  ufilen  19619  rnelfm  19642  fmfnfmlem4  19646  flimcf  19671  fclscf  19714  alexsubALTlem4  19738  ptcmplem3  19742  ptcmplem4  19743  cnextfvval  19753  cnextcn  19755  tmdgsum2  19783  tsmsxplem2  19844  ucnima  19972  ucncn  19976  imasdsf1olem  20064  imasf1oxmet  20066  metss  20199  comet  20204  met2ndci  20213  prdsxmslem2  20220  metustOLD  20258  metust  20259  cfilucfilOLD  20260  cfilucfil  20261  metutopOLD  20273  psmetutop  20274  opnreen  20524  rectbntr0  20525  fsumcn  20562  rescncf  20589  xrhmeo  20634  cnheiborlem  20642  cnheibor  20643  cnllycmp  20644  lebnumlem1  20649  lebnumlem3  20651  ipcau2  20865  tchcphlem1  20866  tchcphlem2  20867  lmmcvg  20888  cfilss  20897  iscmet3lem1  20918  iscmet3lem2  20919  pjthlem1  21040  pjthlem2  21041  ivthlem1  21051  ivthlem2  21052  ivthlem3  21053  ivth2  21055  ivthle  21056  ivthle2  21057  ivthicc  21058  ovolsslem  21083  ovoliunlem1  21101  ovoliunlem2  21102  ovoliunnul  21106  ovolshftlem1  21108  ovolscalem1  21112  ovolicc2lem3  21118  ovolicc2lem4  21119  voliunlem3  21149  volsup  21153  uniiccdif  21174  uniioombllem2  21179  dyadmbl  21196  volivth  21203  vitalilem3  21206  ismbf3d  21248  mbfimaopnlem  21249  cncombf  21252  mbflimsup  21260  i1fd  21275  itg1addlem4  21293  itg2addlem  21352  itg2gt0  21354  iblitg  21362  itgconst  21412  itgfsum  21420  limcvallem  21462  cnlimci  21480  cnmptlimc  21481  limciun  21485  dvadd  21530  dvmul  21531  dvco  21537  dvrec  21545  dvcnv  21565  dvferm1lem  21572  dvferm1  21573  dvferm2lem  21574  dvferm2  21575  dvferm  21576  rollelem  21577  dvlip  21581  dvlipcn  21582  dvlip2  21583  c1liplem1  21584  c1lip2  21586  dvgt0lem1  21590  dvle  21595  dvivthlem1  21596  lhop1lem  21601  dvcnvrelem1  21605  dvcnvrelem2  21606  dvcvx  21608  dvfsumle  21609  dvfsumge  21610  dvfsumabs  21611  dvfsumlem1  21614  dvfsumlem2  21615  dvfsumlem3  21616  dvfsumlem4  21617  dvfsumrlim2  21620  dvfsum2  21622  ftc1cn  21631  ftc2ditglem  21633  itgsubstlem  21636  tdeglem4  21645  mdegaddle  21661  mdegmullem  21665  deg1sublt  21698  ply1divmo  21723  fta1g  21755  dgrub  21818  dgradd2  21851  dvply1  21866  plydivex  21879  plyrem  21887  vieta1lem2  21893  aalioulem4  21917  aalioulem5  21918  aalioulem6  21919  aaliou2  21922  taylf  21942  tayl0  21943  ulmi  21967  ulmdvlem1  21981  ulmdvlem3  21983  ulmdv  21984  mtest  21985  pserulm  22003  psercn2  22004  abelth  22022  abelth2  22023  reeff1olem  22027  efif1olem4  22117  efopn  22219  logreclem  22330  isosctrlem2  22333  rlimcnp  22475  rlimcnp2  22476  xrlimcnp  22478  scvxcvx  22495  wilthlem2  22523  basellem4  22537  ppiwordi  22616  fsumdvdscom  22641  musum  22647  musumsum  22648  chtub  22667  fsumvma  22668  chpub  22675  dchrelbas3  22693  dchrelbasd  22694  dchrn0  22705  dchrptlem2  22720  lgsval2lem  22761  lgsdirnn0  22794  lgsdinn0  22795  2sqlem6  22824  2sqlem10  22829  dchrisumlema  22853  dchrisumlem1  22854  dchrisumlem2  22855  dchrisumlem3  22856  dchrmusum2  22859  dchrvmasumlem2  22863  dchrvmasumlem3  22864  dchrvmasumiflem1  22866  dchrisum0flblem2  22874  dchrisum0flb  22875  dchrisum0re  22878  dchrisum0lem1b  22880  dchrisum0lem2  22883  2vmadivsumlem  22905  chpdifbndlem1  22918  selberg3lem1  22922  selberg4lem1  22925  pntrsumbnd2  22932  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem5  22946  pntrlog2bndlem6  22948  pntibndlem2  22956  pntibndlem3  22957  pntlemn  22965  pntlemj  22968  pntlemi  22969  pntlemo  22972  pntlem3  22974  pntlemp  22975  pntleml  22976  ostth2lem1  22983  ostth2lem2  22999  ostth3  23003  axlowdimlem16  23338  axlowdimlem17  23339  axcontlem3  23347  axcontlem10  23354  usgraedgleord  23447  nbgrassovt  23481  nbgraf1o0  23490  cusgraexg  23512  cusgrafilem2  23523  cusgrafilem3  23524  sizeusglecusg  23529  1conngra  23696  vdusgraval  23712  isgrp2d  23857  opidon  23944  ghgrp  23990  rngodm1dm2  24040  zerdivemp1  24056  ubthlem1  24406  ubthlem2  24407  minvecolem3  24412  minvecolem4b  24414  minvecolem4  24416  bcsiALT  24716  occllem  24841  pjhthlem1  24929  ococin  24946  spanpr  25118  pjorthi  25207  nmbdoplbi  25563  nmcoplbi  25567  nmbdfnlbi  25588  nmcfnlbi  25591  nmopcoi  25634  branmfn  25644  hstnmoc  25762  mdsl0  25849  atomli  25921  atcvat4i  25936  atabsi  25940  abrexdomjm  26023  elpreq  26035  ifeqeqx  26037  fovcld  26089  fnct  26147  xlt2addrd  26185  supxrnemnf  26190  ssnnssfz  26210  resspos  26254  resstos  26255  orngsqr  26406  fmcncfil  26495  xrge0iifiso  26499  elzdif0  26543  qqhval2lem  26544  esumcst  26648  esumpinfval  26656  esumpinfsum  26660  sigaclci  26709  insiga  26714  measres  26770  measdivcstOLD  26772  mbfmcnvima  26806  dya2iocnrect  26830  dya2iocnei  26831  eulerpartlemsv2  26875  eulerpartlemv  26881  eulerpartlemf  26887  eulerpartlemgh  26895  eulerpartlemgs2  26897  ballotlemfp1  27008  ballotlemfrcn0  27046  lgamgulmlem5  27153  lgamcvglem  27160  derangenlem  27193  subfacp1lem3  27204  subfacp1lem5  27206  rescon  27269  cvmliftlem3  27310  cvmlift2lem10  27335  relexpadd  27474  relexpindlem  27475  rtrclreclem.trans  27482  ntrivcvgn0  27547  prodeq2ii  27560  prodmolem3  27580  fprod  27588  fprodmul  27605  fproddiv  27606  fprodm1  27611  fprod1p  27612  fprod2dlem  27625  fprodcom2  27629  wfrlem4  27861  wfrlem15  27872  frrlem4  27905  sltres  27939  nobndlem2  27968  nobndup  27975  nobnddown  27976  nofulllem3  27979  nofulllem5  27981  cgrextend  28173  segconeq  28175  trisegint  28193  ontgval  28411  ftc1cnnclem  28603  ftc1cnnc  28604  ftc2nc  28614  dvasin  28618  dvacos  28619  ivthALT  28668  fnessref  28703  refssfne  28704  comppfsc  28717  neibastop1  28718  filnetlem4  28740  abrexdom  28762  indexdom  28766  mettrifi  28791  equivtotbnd  28815  totbndbnd  28826  prdstotbnd  28831  heibor1lem  28846  bfplem1  28859  bfplem2  28860  zerdivemp1x  28899  mzpsubmpt  29217  mzpsubst  29223  eqrabdioph  29254  rabdiophlem2  29278  elpell14qr2  29341  elpell1qr2  29351  pellfundre  29360  pellfundge  29361  pellfundglb  29364  pellfund14gap  29366  congabseq  29455  dvdsleabs2  29471  jm2.22  29482  jm2.23  29483  jm2.26lem3  29488  wepwsolem  29532  dnwech  29539  aomclem2  29546  aomclem4  29548  dgrnznn  29630  itgpowd  29728  sbiota1  29826  refsumcn  29890  rfcnnnub  29896  fmul01  29899  fmuldfeqlem1  29901  fmuldfeq  29902  fmul01lt1lem1  29903  fmul01lt1lem2  29904  cncfmptss  29906  climinf  29917  climsuselem1  29918  climsuse  29919  stoweidlem3  29936  stoweidlem16  29949  stoweidlem17  29950  stoweidlem19  29952  stoweidlem20  29953  stoweidlem23  29956  stoweidlem25  29958  stoweidlem27  29960  stoweidlem31  29964  stoweidlem34  29967  stoweidlem42  29975  stoweidlem48  29981  stoweidlem51  29984  stoweidlem52  29985  stoweidlem59  29992  wallispilem1  29998  wallispilem3  30000  stirlinglem13  30019  2leaddle2  30313  ige2m2fzo  30358  wwlktovfo  30391  wrd2f1tovbij  30393  nbgrassvwo  30414  usgra2wlkspth  30436  usgra2pthlem1  30438  usgra2adedgwlk  30444  usgra2adedgwlkon  30445  wlkiswwlk2lem3  30465  wwlkextbij  30503  wwlkexthasheq  30504  clwlkisclwwlklem0  30588  wwlksubclwwlk  30604  clwwisshclwwlem1  30607  eleclclwwlknlem1  30628  eleclclwwlknlem2  30629  Lemma2  30631  usg2cwwkdifex  30633  clwlkfclwwlk  30655  clwlkf1clwwlklem  30660  clwlksizeeq  30663  rusgranumwlkl1lem1  30696  rusgranumwlklem4  30708  rusgra0edg  30711  rusgranumwwlkg  30715  frgranbnb  30750  frgrancvvdeqlem3  30763  frgrancvvdeqlem9  30772  frg2woteu  30786  frg2woteqm  30790  usgreghash2spotv  30797  numclwwlkovf2ex  30817  numclwlk1lem2fo  30826  numclwwlkqhash  30831  numclwwlk2lem1  30833  numclwlk2lem2f  30834  numclwwlk2lem3  30837  numclwwlk5  30843  numclwwlk7  30845  a2and  30854  ssnn0ssfz  30879  supgtoreq  30881  fsuppmapnn0fiubex  30938  nn0gsumfz  30945  telescgsum  30955  mptcoe1fsupp  30975  cply1coe0bi  30992  mat0dimscm  31019  ldepspr  31114  cpmatmcllem  31181  mptcoe1matfsupp  31249  mp2pm2mp  31266  cpdmat  31295  chmaidscmat  31302  ordelordALT  31544  2pm13.193  31561  ee11an  31712  eel2221  31725  bnj1379  32124  bnj580  32206  bnj944  32231  bnj999  32250  bnj1204  32303  bnj1398  32325  bj-babygodel  32423  bj-finsumval0  32889  omllaw5N  33198  cmtcomlemN  33199  cmtbr3N  33205  omlfh3N  33210  atlen0  33261  exatleN  33354  hlrelat3  33362  cvrexchlem  33369  atlelt  33388  cvrat4  33393  4atlem11b  33558  4atlem12b  33561  lneq2at  33728  cdlema1N  33741  cdlemblem  33743  paddss12  33769  paddasslem2  33771  paddasslem4  33773  paddasslem6  33775  paddasslem12  33781  paddunN  33877  poml4N  33903  poml5N  33904  osumcllem6N  33911  pexmidlem6N  33925  pl42lem2N  33930  ltrnu  34071  ltrneq2  34098  trlval2  34113  cdlemd6  34153  cdleme25b  34304  cdleme29b  34325  cdlemefr29exN  34352  ltrniotacnvval  34532  cdlemk28-3  34858  dochexmidlem7  35417
  Copyright terms: Public domain W3C validator