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  529  syl2anc  654  nfimd  1848  ax13fromc9  2207  equid1  2209  elex2  2974  elex22  2975  spcimdv  3043  spsbcd  3188  disjxiun  4277  reusv2lem3  4483  opth  4554  euotd  4580  wereu  4703  wereu2  4704  tz7.7  4732  unielrel  5350  funmo  5422  iinpreima  5821  fnfvima  5942  fliftfun  5992  fliftval  5996  weniso  6032  knatar  6035  riota5f  6065  riotass2  6067  grprinvlem  6290  grprinvd  6291  ofmpteq  6327  caofref  6335  ssorduni  6386  suceloni  6413  nlimsucg  6442  tfisi  6458  zfrep6  6534  curry1  6653  curry2  6656  fnwelem  6676  funsssuppss  6704  smogt  6814  tfrlem1  6821  tfrlem5  6825  omeulem1  7009  oeworde  7020  oelimcl  7027  oeeulem  7028  oeeui  7029  nnawordex  7064  oaabs2  7072  ertr  7104  swoso  7120  qliftlem  7169  th3q  7197  resixp  7286  f1dom2g  7315  dom3d  7339  undom  7387  xpdom3  7397  domunsncan  7399  omxpenlem  7400  disjenex  7457  domssex2  7459  domssex  7460  xpf1o  7461  mapdom3  7471  findcard  7539  fiin  7660  marypha1lem  7671  marypha1  7672  fisupcl  7705  ordiso2  7717  ordtypelem2  7721  ordtypelem6  7725  ordtypelem7  7726  ordtypelem8  7727  wemapso2OLD  7754  wemapso2lem  7755  brwdom2  7776  unxpwdom2  7791  noinfepOLD  7854  cantnflt  7868  cantnfrescl  7872  oemapvali  7880  cantnflem1d  7884  cantnfltOLD  7898  cantnflem1dOLD  7907  wemapwe  7916  wemapweOLD  7917  cnfcom  7921  cnfcomOLD  7929  rankr1id  8057  tcrank  8079  cardmin2  8156  infxpenlem  8168  infxpenc2lem2  8174  infxpenc2lem2OLD  8178  fseqen  8185  dfac8clem  8190  ween  8193  ac5num  8194  indcardi  8199  acni  8203  acni2  8204  acnlem  8206  fodomfi2  8218  infpwfien  8220  inffien  8221  finnisoeu  8271  iunfictbso  8272  acacni  8297  dfac12lem2  8301  infpss  8374  infmap2  8375  ackbij1lem18  8394  ackbij1b  8396  fictb  8402  cfslb2n  8425  cofsmo  8426  cfsmolem  8427  coftr  8430  fin1ai  8450  fin2i  8452  infpssrlem4  8463  domfin4  8468  fin2i2  8475  isfin2-2  8476  fincssdom  8480  ssfin3ds  8487  fin23lem20  8494  fin23lem30  8499  isf32lem3  8512  fin1a2lem12  8568  fin1a2lem13  8569  hsmexlem2  8584  hsmexlem4  8586  axdc2lem  8605  axdc4lem  8612  ac6num  8636  ttukeylem6  8671  axdclem2  8677  imadomg  8689  iundom2g  8692  iundomg  8693  iundom  8694  unirnfdomd  8719  konigthlem  8720  iunctb  8726  fpwwe2  8798  canth4  8802  canthwelem  8805  pwfseqlem3  8815  pwfseqlem5  8818  winalim2  8851  wununi  8861  wunpw  8862  wunelss  8863  r1wunlim  8892  wunex2  8893  tsksdom  8911  tskinf  8924  inttsk  8929  inar1  8930  tskcard  8936  tskurn  8944  gruina  8973  grur1a  8974  grur1  8975  dedekind  9521  lemul12a  10175  lemulge11  10179  lediv12a  10213  nngt0  10339  peano5uzi  10718  nn0ind-raph  10730  zsupss  10932  suprzub  10934  uzsupss  10935  uzwo3  10936  rpge0  10991  fz0fzelfz0  11473  fz0fzdiffz0  11476  elfzodifsumelfzo  11588  fzonfzoufzol  11612  flltdivnn0lt  11661  fldiv  11683  modaddmodup  11746  uzrdgsuci  11767  fzennn  11774  uzindi  11787  seqcl2  11808  seqcl  11810  seqf  11811  seqfveq2  11812  seqfveq  11814  seqshft2  11816  monoord  11820  monoord2  11821  sermono  11822  seqsplit  11823  seqcaopr3  11825  seqid  11835  seqid2  11836  seqhomo  11837  seqz  11838  expcl2lem  11861  leexp1a  11906  modexp  11983  discr1  11984  discr  11985  faclbnd  12050  faclbnd6  12059  facavg  12061  hashginv  12091  hashf1rn  12107  hashge2el2dif  12168  hashimarn  12184  hashbclem  12189  fz1isolem  12198  seqcoll  12200  wrdsymb0  12243  wrdlenge2n0  12245  lsw0  12251  ccatsymb  12265  swrdvalodm2  12317  swrdvalodm  12318  swrdswrd0  12340  swrd0swrd0  12341  wrd2ind  12356  swrdccatin12  12366  swrdccat3  12367  swrdccat  12368  swrdccatid  12372  swrdccatin1d  12374  swrdccatin12d  12376  repswswrd  12406  cshwidxmod  12424  s2f1o  12510  f1oun2prg  12511  resqrex  12724  cau3lem  12826  limsupgre  12943  climi  12972  rlimi  12975  rlimclim  13008  climrlim2  13009  rlimcld2  13040  rlimcn1  13050  climcn1  13053  climcn2  13054  isercoll  13129  isercoll2  13130  climsup  13131  caucvgrlem  13134  caurcvgr  13135  iseraltlem2  13144  iseraltlem3  13145  sumeq2ii  13154  summolem3  13175  zsum  13179  fsum  13181  fsumadd  13199  fsumm1  13204  fsum1p  13206  fsum2dlem  13221  fsumcom2  13225  fsum0diag2  13233  fsummulc2  13234  fsumge1  13243  fsumabs  13247  fsumtscopo  13248  fsumtscopo2  13249  fsumparts  13252  fsumrelem  13253  fsumrlim  13257  fsumo1  13258  o1fsum  13259  fsumiun  13267  qshash  13273  isum1p  13287  isumrpcl  13289  climcndslem1  13295  climcndslem2  13296  climcnds  13297  cvgrat  13326  mertenslem1  13327  mertens  13329  sin01gt0  13457  sin02gt0  13459  efieq1re  13466  divalglem9  13588  smupvallem  13662  rppwr  13724  algfx  13738  eucalgcvga  13744  prmind2  13757  qredeq  13775  modprm0  13856  pythagtriplem4  13869  pythagtriplem6  13871  pythagtriplem7  13872  pythagtriplem12  13876  pythagtriplem13  13877  pythagtriplem14  13878  pythagtriplem16  13880  pcmpt  13937  pcmpt2  13938  prmpwdvds  13948  prmreclem2  13961  prmreclem4  13963  prmreclem5  13964  4sqlem11  13999  vdwlem1  14025  vdwlem2  14026  vdwlem9  14033  vdwlem10  14034  vdwlem11  14035  vdwlem12  14036  rami  14059  0ram  14064  0ram2  14065  0ramcl  14067  ramcl  14073  cshwsidrepsw  14103  cshwshashlem2  14106  prmlem1  14118  prmlem2  14130  strfvd  14188  strfv2d  14189  strssd  14193  firest  14354  prdsdsval3  14406  imasbas  14433  imasds  14434  imasaddfnlem  14449  imasaddvallem  14450  imasvscafn  14458  divsaddvallem  14472  divsaddflem  14473  divsaddval  14474  divsaddf  14475  divsmulval  14476  divsmulf  14477  isacs1i  14578  mreacs  14579  catidex  14595  catideu  14596  iscatd2  14602  catlid  14604  catrid  14605  subcidcl  14737  funcid  14763  invfuc  14867  yonedalem4c  15070  yonffthlem  15075  mod2ile  15259  lubss  15274  acsmapd  15331  mrcmndind  15476  gsumval2a  15492  grpidd2  15555  mulgnegnn  15617  mulgsubcl  15621  divsgrp2  15653  issubg4  15680  ghmf1  15755  pgrpsubgsymg  15893  fvcosymgeq  15914  gsmsymgreqlem1  15915  psgnunilem4  15983  pgpssslw  16093  sylow2alem2  16097  fislw  16104  efgsdmi  16209  efgsrel  16211  efgsres  16215  gexexlem  16314  gsumval3OLD  16362  gsumval3lem2  16364  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsummhm2  16411  gsummhm2OLD  16412  gsum2d  16437  gsum2dOLD  16438  dprddomcld  16457  dprdcntz  16466  dprddisj  16467  dprdss  16500  dprd2dlem2  16513  dprd2da  16515  dpjrid  16535  ablfac1eu  16548  pgpfac1lem1  16549  ablfac2  16564  rngi  16593  divsrng2  16647  issrngd  16870  lssintcl  16967  islbs2  17157  lbsextlem3  17163  lbsextlem4  17164  mplsubglem  17444  mpllsslem  17445  mplsubglemOLD  17446  mpllsslemOLD  17447  subrgasclcl  17513  zringlpirlem3  17747  zlpirlem3  17752  psgnodpm  17860  psgndiflemB  17872  frlmphl  18048  frlmup4  18071  lindff1  18091  lindfrn  18092  lmisfree  18113  mdetralt  18256  mdetunilem9  18268  slesolinv  18328  cramerimp  18334  eltg3  18409  cctop  18452  subbascn  18700  iscncl  18715  cnss2  18723  cnrmi  18806  cmpcov  18834  cmpcovf  18836  fiuncmp  18849  2ndcctbss  18901  2ndcomap  18904  2ndcsep  18905  1stcelcls  18907  islly2  18930  ptpjpre1  18986  elptr  18988  ptbasfi  18996  ptpjopn  19027  ptclsg  19030  dfac14  19033  txcnp  19035  ptcnplem  19036  uptx  19040  txtube  19055  tx2ndc  19066  xkococnlem  19074  cnmpt11  19078  cnmpt21  19086  cnmptkp  19095  cnmptk1p  19100  elqtop  19112  qtoprest  19132  qtopomap  19133  qtopcmap  19134  indishmph  19213  ptcmpfi  19228  kqhmph  19234  csdfil  19309  filssufilg  19326  ufilen  19345  rnelfm  19368  fmfnfmlem4  19372  flimcf  19397  fclscf  19440  alexsubALTlem4  19464  ptcmplem3  19468  ptcmplem4  19469  cnextfvval  19479  cnextcn  19481  tmdgsum2  19509  tsmsxplem2  19570  ucnima  19698  ucncn  19702  imasdsf1olem  19790  imasf1oxmet  19792  metss  19925  comet  19930  met2ndci  19939  prdsxmslem2  19946  metustOLD  19984  metust  19985  cfilucfilOLD  19986  cfilucfil  19987  metutopOLD  19999  psmetutop  20000  opnreen  20250  rectbntr0  20251  fsumcn  20288  rescncf  20315  xrhmeo  20360  cnheiborlem  20368  cnheibor  20369  cnllycmp  20370  lebnumlem1  20375  lebnumlem3  20377  ipcau2  20591  tchcphlem1  20592  tchcphlem2  20593  lmmcvg  20614  cfilss  20623  iscmet3lem1  20644  iscmet3lem2  20645  pjthlem1  20766  pjthlem2  20767  ivthlem1  20777  ivthlem2  20778  ivthlem3  20779  ivth2  20781  ivthle  20782  ivthle2  20783  ivthicc  20784  ovolsslem  20809  ovoliunlem1  20827  ovoliunlem2  20828  ovoliunnul  20832  ovolshftlem1  20834  ovolscalem1  20838  ovolicc2lem3  20844  ovolicc2lem4  20845  voliunlem3  20875  volsup  20879  uniiccdif  20900  uniioombllem2  20905  dyadmbl  20922  volivth  20929  vitalilem3  20932  ismbf3d  20974  mbfimaopnlem  20975  cncombf  20978  mbflimsup  20986  i1fd  21001  itg1addlem4  21019  itg2addlem  21078  itg2gt0  21080  iblitg  21088  itgconst  21138  itgfsum  21146  limcvallem  21188  cnlimci  21206  cnmptlimc  21207  limciun  21211  dvadd  21256  dvmul  21257  dvco  21263  dvrec  21271  dvcnv  21291  dvferm1lem  21298  dvferm1  21299  dvferm2lem  21300  dvferm2  21301  dvferm  21302  rollelem  21303  dvlip  21307  dvlipcn  21308  dvlip2  21309  c1liplem1  21310  c1lip2  21312  dvgt0lem1  21316  dvle  21321  dvivthlem1  21322  lhop1lem  21327  dvcnvrelem1  21331  dvcnvrelem2  21332  dvcvx  21334  dvfsumle  21335  dvfsumge  21336  dvfsumabs  21337  dvfsumlem1  21340  dvfsumlem2  21341  dvfsumlem3  21342  dvfsumlem4  21343  dvfsumrlim2  21346  dvfsum2  21348  ftc1cn  21357  ftc2ditglem  21359  itgsubstlem  21362  evlslem3  21366  evlseu  21368  mpfpf1  21402  pf1mpf  21403  tdeglem4  21414  mdegaddle  21430  mdegmullem  21434  deg1sublt  21467  ply1divmo  21492  fta1g  21524  dgrub  21587  dgradd2  21620  dvply1  21635  plydivex  21648  plyrem  21656  vieta1lem2  21662  aalioulem4  21686  aalioulem5  21687  aalioulem6  21688  aaliou2  21691  taylf  21711  tayl0  21712  ulmi  21736  ulmdvlem1  21750  ulmdvlem3  21752  ulmdv  21753  mtest  21754  pserulm  21772  psercn2  21773  abelth  21791  abelth2  21792  reeff1olem  21796  efif1olem4  21886  efopn  21988  logreclem  22099  isosctrlem2  22102  rlimcnp  22244  rlimcnp2  22245  xrlimcnp  22247  scvxcvx  22264  wilthlem2  22292  basellem4  22306  ppiwordi  22385  fsumdvdscom  22410  musum  22416  musumsum  22417  chtub  22436  fsumvma  22437  chpub  22444  dchrelbas3  22462  dchrelbasd  22463  dchrn0  22474  dchrptlem2  22489  lgsval2lem  22530  lgsdirnn0  22563  lgsdinn0  22564  2sqlem6  22593  2sqlem10  22598  dchrisumlema  22622  dchrisumlem1  22623  dchrisumlem2  22624  dchrisumlem3  22625  dchrmusum2  22628  dchrvmasumlem2  22632  dchrvmasumlem3  22633  dchrvmasumiflem1  22635  dchrisum0flblem2  22643  dchrisum0flb  22644  dchrisum0re  22647  dchrisum0lem1b  22649  dchrisum0lem2  22652  2vmadivsumlem  22674  chpdifbndlem1  22687  selberg3lem1  22691  selberg4lem1  22694  pntrsumbnd2  22701  pntrlog2bndlem2  22712  pntrlog2bndlem3  22713  pntrlog2bndlem5  22715  pntrlog2bndlem6  22717  pntibndlem2  22725  pntibndlem3  22726  pntlemn  22734  pntlemj  22737  pntlemi  22738  pntlemo  22741  pntlem3  22743  pntlemp  22744  pntleml  22745  ostth2lem1  22752  ostth2lem2  22768  ostth3  22772  axlowdimlem16  23026  axlowdimlem17  23027  axcontlem3  23035  axcontlem10  23042  usgraedgleord  23135  nbgrassovt  23169  nbgraf1o0  23178  cusgraexg  23200  cusgrafilem2  23211  cusgrafilem3  23212  sizeusglecusg  23217  1conngra  23384  vdusgraval  23400  isgrp2d  23545  opidon  23632  ghgrp  23678  rngodm1dm2  23728  zerdivemp1  23744  ubthlem1  24094  ubthlem2  24095  minvecolem3  24100  minvecolem4b  24102  minvecolem4  24104  bcsiALT  24404  occllem  24529  pjhthlem1  24617  ococin  24634  spanpr  24806  pjorthi  24895  nmbdoplbi  25251  nmcoplbi  25255  nmbdfnlbi  25276  nmcfnlbi  25279  nmopcoi  25322  branmfn  25332  hstnmoc  25450  mdsl0  25537  atomli  25609  atcvat4i  25624  atabsi  25628  abrexdomjm  25712  elpreq  25724  ifeqeqx  25726  fovcld  25779  fnct  25837  xlt2addrd  25876  supxrnemnf  25879  ssnnssfz  25899  resspos  25943  resstos  25944  srgi  26047  orngsqr  26125  fmcncfil  26215  xrge0iifiso  26219  elzdif0  26263  qqhval2lem  26264  esumcst  26368  esumpinfval  26376  esumpinfsum  26380  sigaclci  26429  insiga  26434  measres  26490  measdivcstOLD  26492  mbfmcnvima  26526  dya2iocnrect  26550  dya2iocnei  26551  eulerpartlemsv2  26589  eulerpartlemv  26595  eulerpartlemf  26601  eulerpartlemgh  26609  eulerpartlemgs2  26611  ballotlemfp1  26722  ballotlemfrcn0  26760  lgamgulmlem5  26867  lgamcvglem  26874  derangenlem  26907  subfacp1lem3  26918  subfacp1lem5  26920  rescon  26983  cvmliftlem3  27024  cvmlift2lem10  27049  relexpadd  27187  relexpindlem  27188  rtrclreclem.trans  27195  ntrivcvgn0  27260  prodeq2ii  27273  prodmolem3  27293  fprod  27301  fprodmul  27318  fproddiv  27319  fprodm1  27324  fprod1p  27325  fprod2dlem  27338  fprodcom2  27342  wfrlem4  27574  wfrlem15  27585  frrlem4  27618  sltres  27652  nobndlem2  27681  nobndup  27688  nobnddown  27689  nofulllem3  27692  nofulllem5  27694  cgrextend  27886  segconeq  27888  trisegint  27906  ontgval  28125  ftc1cnnclem  28309  ftc1cnnc  28310  ftc2nc  28320  dvasin  28324  dvacos  28325  ivthALT  28374  fnessref  28409  refssfne  28410  comppfsc  28423  neibastop1  28424  filnetlem4  28446  abrexdom  28468  indexdom  28472  mettrifi  28497  equivtotbnd  28521  totbndbnd  28532  prdstotbnd  28537  heibor1lem  28552  bfplem1  28565  bfplem2  28566  zerdivemp1x  28605  mzpsubmpt  28924  mzpsubst  28930  eqrabdioph  28961  rabdiophlem2  28985  elpell14qr2  29048  elpell1qr2  29058  pellfundre  29067  pellfundge  29068  pellfundglb  29071  pellfund14gap  29073  congabseq  29162  dvdsleabs2  29178  jm2.22  29189  jm2.23  29190  jm2.26lem3  29195  wepwsolem  29239  dnwech  29246  aomclem2  29253  aomclem4  29255  dgrnznn  29337  itgpowd  29435  sbiota1  29533  refsumcn  29597  rfcnnnub  29603  fmul01  29606  fmuldfeqlem1  29608  fmuldfeq  29609  fmul01lt1lem1  29610  fmul01lt1lem2  29611  cncfmptss  29613  climinf  29625  climsuselem1  29626  climsuse  29627  stoweidlem3  29644  stoweidlem16  29657  stoweidlem17  29658  stoweidlem19  29660  stoweidlem20  29661  stoweidlem23  29664  stoweidlem25  29666  stoweidlem27  29668  stoweidlem31  29672  stoweidlem34  29675  stoweidlem42  29683  stoweidlem48  29689  stoweidlem51  29692  stoweidlem52  29693  stoweidlem59  29700  wallispilem1  29706  wallispilem3  29708  stirlinglem13  29727  2leaddle2  30021  ige2m2fzo  30066  wwlktovfo  30099  wrd2f1tovbij  30101  nbgrassvwo  30122  usgra2wlkspth  30144  usgra2pthlem1  30146  usgra2adedgwlk  30152  usgra2adedgwlkon  30153  wlkiswwlk2lem3  30173  wwlkextbij  30211  wwlkexthasheq  30212  clwlkisclwwlklem0  30296  wwlksubclwwlk  30312  clwwisshclwwlem1  30315  eleclclwwlknlem1  30336  eleclclwwlknlem2  30337  Lemma2  30339  usg2cwwkdifex  30341  clwlkfclwwlk  30363  clwlkf1clwwlklem  30368  clwlksizeeq  30371  rusgranumwlkl1lem1  30404  rusgranumwlklem4  30416  rusgra0edg  30419  rusgranumwwlkg  30423  frgranbnb  30458  frgrancvvdeqlem3  30471  frgrancvvdeqlem9  30480  frg2woteu  30494  frg2woteqm  30498  usgreghash2spotv  30505  numclwwlkovf2ex  30525  numclwlk1lem2fo  30534  numclwwlkqhash  30539  numclwwlk2lem1  30541  numclwlk2lem2f  30542  numclwwlk2lem3  30545  numclwwlk5  30551  numclwwlk7  30553  mat0dimscm  30645  ldepspr  30716  ordelordALT  30945  2pm13.193  30962  ee11an  31114  eel2221  31127  bnj1379  31526  bnj580  31608  bnj944  31633  bnj999  31652  bnj1204  31705  bnj1398  31727  bj-babygodel  31785  bj-finsumval0  32159  omllaw5N  32465  cmtcomlemN  32466  cmtbr3N  32472  omlfh3N  32477  atlen0  32528  exatleN  32621  hlrelat3  32629  cvrexchlem  32636  atlelt  32655  cvrat4  32660  4atlem11b  32825  4atlem12b  32828  lneq2at  32995  cdlema1N  33008  cdlemblem  33010  paddss12  33036  paddasslem2  33038  paddasslem4  33040  paddasslem6  33042  paddasslem12  33048  paddunN  33144  poml4N  33170  poml5N  33171  osumcllem6N  33178  pexmidlem6N  33192  pl42lem2N  33197  ltrnu  33338  ltrneq2  33365  trlval2  33380  cdlemd6  33420  cdleme25b  33571  cdleme29b  33592  cdlemefr29exN  33619  ltrniotacnvval  33799  cdlemk28-3  34125  dochexmidlem7  34684
  Copyright terms: Public domain W3C validator