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

Theorem sylc 58
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 36 . 2  |-  ( ph  ->  ( ph  ->  th )
)
54pm2.43i 45 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl3c  59  mpsyl  61  jc  141  2thd  232  jca  519  syl2anc  643  nfimd  1823  ax12OLD  1986  ax12from12o  2206  equid1  2208  elex22  2927  elex2  2928  spcimdv  2993  spsbcd  3134  disjxiun  4169  opth  4395  euotd  4417  wereu  4538  wereu2  4539  tz7.7  4567  reusv2lem3  4685  ssorduni  4725  suceloni  4752  nlimsucg  4781  tfisi  4797  unielrel  5353  funmo  5429  iinpreima  5819  zfrep6  5927  fnfvima  5935  fliftfun  5993  fliftval  5997  weniso  6034  knatar  6039  grprinvlem  6244  grprinvd  6245  caofref  6289  curry1  6397  curry2  6400  fnwelem  6420  riota5f  6533  riotass2  6536  smogt  6588  omeulem1  6784  oeworde  6795  oelimcl  6802  oeeulem  6803  oeeui  6804  nnawordex  6839  oaabs2  6847  ertr  6879  swoso  6895  qliftlem  6944  th3q  6972  resixp  7056  f1dom2g  7084  dom3d  7108  undom  7155  xpdom3  7165  domunsncan  7167  omxpenlem  7168  disjenex  7224  domssex2  7226  domssex  7227  xpf1o  7228  mapdom3  7238  findcard  7306  fiin  7385  marypha1lem  7396  marypha1  7397  fisupcl  7428  ordiso2  7440  ordtypelem2  7444  ordtypelem6  7448  ordtypelem7  7449  ordtypelem8  7450  wemapso2  7477  brwdom2  7497  unxpwdom2  7512  noinfepOLD  7571  cantnflt  7583  oemapvali  7596  cantnflem1d  7600  wemapwe  7610  cnfcom  7613  rankr1id  7744  tcrank  7764  cardmin2  7841  infxpenlem  7851  infxpenc2lem2  7857  fseqen  7864  dfac8clem  7869  ween  7872  ac5num  7873  indcardi  7878  acni  7882  acni2  7883  acnlem  7885  fodomfi2  7897  infpwfien  7899  inffien  7900  finnisoeu  7950  iunfictbso  7951  acacni  7976  dfac12lem2  7980  infpss  8053  infmap2  8054  ackbij1lem18  8073  ackbij1b  8075  fictb  8081  cfslb2n  8104  cofsmo  8105  cfsmolem  8106  coftr  8109  fin1ai  8129  fin2i  8131  infpssrlem4  8142  domfin4  8147  fin2i2  8154  isfin2-2  8155  fincssdom  8159  ssfin3ds  8166  fin23lem20  8173  fin23lem30  8178  isf32lem3  8191  fin1a2lem12  8247  fin1a2lem13  8248  hsmexlem2  8263  hsmexlem4  8265  axdc2lem  8284  axdc4lem  8291  ac6num  8315  ttukeylem6  8350  axdclem2  8356  imadomg  8368  iundom2g  8371  iundomg  8372  iundom  8373  unirnfdomd  8398  konigthlem  8399  iunctb  8405  fpwwe2  8474  canth4  8478  canthwelem  8481  pwfseqlem3  8491  pwfseqlem5  8494  winalim2  8527  wununi  8537  wunpw  8538  wunelss  8539  r1wunlim  8568  wunex2  8569  tsksdom  8587  tskinf  8600  inttsk  8605  inar1  8606  tskcard  8612  tskurn  8620  gruina  8649  grur1a  8650  grur1  8651  lemul12a  9824  lemulge11  9828  lediv12a  9859  nngt0  9985  peano5uzi  10314  nn0ind-raph  10326  zsupss  10521  suprzub  10523  uzsupss  10524  uzwo3  10525  rpge0  10580  fldiv  11196  uzrdgsuci  11255  fzennn  11262  uzindi  11275  seqcl2  11296  seqcl  11298  seqf  11299  seqfveq2  11300  seqfveq  11302  seqshft2  11304  monoord  11308  monoord2  11309  sermono  11310  seqsplit  11311  seqcaopr3  11313  seqid  11323  seqid2  11324  seqhomo  11325  seqz  11326  expcl2lem  11348  leexp1a  11393  modexp  11469  discr1  11470  discr  11471  faclbnd  11536  faclbnd6  11545  facavg  11547  hashginv  11577  hashf1rn  11591  hashbclem  11656  fz1isolem  11665  seqcoll  11667  s2f1o  11818  f1oun2prg  11819  resqrex  12011  cau3lem  12113  limsupgre  12230  climi  12259  rlimi  12262  rlimclim  12295  climrlim2  12296  rlimcld2  12327  rlimcn1  12337  climcn1  12340  climcn2  12341  isercoll  12416  isercoll2  12417  climsup  12418  caucvgrlem  12421  caurcvgr  12422  iseraltlem2  12431  iseraltlem3  12432  sumeq2ii  12442  summolem3  12463  fsum  12469  fsumadd  12487  fsumm1  12492  fsum1p  12494  fsum2dlem  12509  fsumcom2  12513  fsum0diag2  12521  fsummulc2  12522  fsumge1  12531  fsumabs  12535  fsumtscopo  12536  fsumtscopo2  12537  fsumparts  12540  fsumrelem  12541  fsumrlim  12545  fsumo1  12546  o1fsum  12547  fsumiun  12555  qshash  12561  isum1p  12576  isumrpcl  12578  climcndslem1  12584  climcndslem2  12585  climcnds  12586  cvgrat  12615  mertenslem1  12616  mertens  12618  sin01gt0  12746  sin02gt0  12748  efieq1re  12755  divalglem9  12876  smupvallem  12950  rppwr  13012  algfx  13026  eucalgcvga  13032  prmind2  13045  qredeq  13061  pythagtriplem4  13148  pythagtriplem6  13150  pythagtriplem7  13151  pythagtriplem12  13155  pythagtriplem13  13156  pythagtriplem14  13157  pythagtriplem16  13159  pcmpt  13216  pcmpt2  13217  prmpwdvds  13227  prmreclem2  13240  prmreclem4  13242  prmreclem5  13243  4sqlem11  13278  vdwlem1  13304  vdwlem2  13305  vdwlem9  13312  vdwlem10  13313  vdwlem11  13314  vdwlem12  13315  rami  13338  0ram  13343  0ram2  13344  0ramcl  13346  ramcl  13352  prmlem1  13385  prmlem2  13397  strfvd  13453  strfv2d  13454  strssd  13458  firest  13615  prdsdsval3  13662  imasbas  13693  imasds  13694  imasaddfnlem  13708  imasaddvallem  13709  imasvscafn  13717  divsaddvallem  13731  divsaddflem  13732  divsaddval  13733  divsaddf  13734  divsmulval  13735  divsmulf  13736  isacs1i  13837  mreacs  13838  catidex  13854  catideu  13855  iscatd2  13861  catlid  13863  catrid  13864  subcidcl  13996  funcid  14022  invfuc  14126  yonedalem4c  14329  yonffthlem  14334  mod2ile  14490  lubss  14503  acsmapd  14559  gsumval2a  14737  grpidd2  14797  mulgnegnn  14855  mulgsubcl  14859  divsgrp2  14891  issubg4  14916  ghmf1  14989  pgpssslw  15203  sylow2alem2  15207  fislw  15214  efgsdmi  15319  efgsrel  15321  efgsres  15325  gexexlem  15422  gsumval3  15469  gsumzaddlem  15481  gsummhm2  15490  gsum2d  15501  dprdcntz  15521  dprddisj  15522  dprdss  15542  dprd2dlem2  15553  dprd2da  15555  dpjrid  15575  ablfac1eu  15586  pgpfac1lem1  15587  ablfac2  15602  rngi  15631  divsrng2  15681  issrngd  15904  lssintcl  15995  islbs2  16181  lbsextlem3  16187  lbsextlem4  16188  mplsubglem  16453  mpllsslem  16454  subrgasclcl  16514  zlpirlem3  16725  eltg3  16982  cctop  17025  subbascn  17272  iscncl  17287  cnss2  17295  cnrmi  17378  cmpcov  17406  cmpcovf  17408  fiuncmp  17421  2ndcctbss  17471  2ndcomap  17474  2ndcsep  17475  1stcelcls  17477  islly2  17500  ptpjpre1  17556  elptr  17558  ptbasfi  17566  ptpjopn  17597  ptclsg  17600  dfac14  17603  txcnp  17605  ptcnplem  17606  uptx  17610  txtube  17625  tx2ndc  17636  xkococnlem  17644  cnmpt11  17648  cnmpt21  17656  cnmptkp  17665  cnmptk1p  17670  elqtop  17682  qtoprest  17702  qtopomap  17703  qtopcmap  17704  indishmph  17783  ptcmpfi  17798  kqhmph  17804  csdfil  17879  filssufilg  17896  ufilen  17915  rnelfm  17938  fmfnfmlem4  17942  flimcf  17967  fclscf  18010  alexsubALTlem4  18034  ptcmplem3  18038  ptcmplem4  18039  cnextfvval  18049  cnextcn  18051  tmdgsum2  18079  tsmsxplem2  18136  ucnima  18264  ucncn  18268  imasdsf1olem  18356  imasf1oxmet  18358  metss  18491  comet  18496  met2ndci  18505  prdsxmslem2  18512  metustOLD  18550  metust  18551  cfilucfilOLD  18552  cfilucfil  18553  metutopOLD  18565  psmetutop  18566  opnreen  18815  rectbntr0  18816  fsumcn  18853  rescncf  18880  xrhmeo  18924  cnheiborlem  18932  cnheibor  18933  cnllycmp  18934  lebnumlem1  18939  lebnumlem3  18941  ipcau2  19144  tchcphlem1  19145  tchcphlem2  19146  lmmcvg  19167  cfilss  19176  iscmet3lem1  19197  iscmet3lem2  19198  pjthlem1  19291  pjthlem2  19292  ivthlem1  19301  ivthlem2  19302  ivthlem3  19303  ivth2  19305  ivthle  19306  ivthle2  19307  ivthicc  19308  ovolsslem  19333  ovoliunlem1  19351  ovoliunlem2  19352  ovoliunnul  19356  ovolshftlem1  19358  ovolscalem1  19362  ovolicc2lem3  19368  ovolicc2lem4  19369  voliunlem3  19399  volsup  19403  uniiccdif  19423  uniioombllem2  19428  dyadmbl  19445  volivth  19452  vitalilem3  19455  ismbf3d  19499  mbfimaopnlem  19500  cncombf  19503  mbflimsup  19511  i1fd  19526  itg1addlem4  19544  itg2addlem  19603  itg2gt0  19605  iblitg  19613  itgconst  19663  itgfsum  19671  limcvallem  19711  cnlimci  19729  cnmptlimc  19730  limciun  19734  dvadd  19779  dvmul  19780  dvco  19786  dvrec  19794  dvcnv  19814  dvferm1lem  19821  dvferm1  19822  dvferm2lem  19823  dvferm2  19824  dvferm  19825  rollelem  19826  dvlip  19830  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  c1lip2  19835  dvgt0lem1  19839  dvle  19844  dvivthlem1  19845  lhop1lem  19850  dvcnvrelem1  19854  dvcnvrelem2  19855  dvcvx  19857  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem1  19863  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumlem4  19866  dvfsumrlim2  19869  dvfsum2  19871  ftc1cn  19880  ftc2ditglem  19882  itgsubstlem  19885  evlslem3  19888  evlseu  19890  mpfpf1  19924  pf1mpf  19925  tdeglem4  19936  mdegaddle  19950  mdegmullem  19954  deg1sublt  19986  ply1divmo  20011  fta1g  20043  dgrub  20106  dgradd2  20139  dvply1  20154  plydivex  20167  plyrem  20175  vieta1lem2  20181  aalioulem4  20205  aalioulem5  20206  aalioulem6  20207  aaliou2  20210  taylf  20230  tayl0  20231  ulmi  20255  ulmdvlem1  20269  ulmdvlem3  20271  ulmdv  20272  mtest  20273  pserulm  20291  psercn2  20292  abelth  20310  abelth2  20311  reeff1olem  20315  efif1olem4  20400  efopn  20502  logreclem  20613  isosctrlem2  20616  rlimcnp  20757  rlimcnp2  20758  xrlimcnp  20760  scvxcvx  20777  wilthlem2  20805  basellem4  20819  ppiwordi  20898  fsumdvdscom  20923  musum  20929  musumsum  20930  chtub  20949  fsumvma  20950  chpub  20957  dchrelbas3  20975  dchrelbasd  20976  dchrn0  20987  dchrptlem2  21002  lgsval2lem  21043  lgsdirnn0  21076  lgsdinn0  21077  2sqlem6  21106  2sqlem10  21111  dchrisumlema  21135  dchrisumlem1  21136  dchrisumlem2  21137  dchrisumlem3  21138  dchrmusum2  21141  dchrvmasumlem2  21145  dchrvmasumlem3  21146  dchrvmasumiflem1  21148  dchrisum0flblem2  21156  dchrisum0flb  21157  dchrisum0re  21160  dchrisum0lem1b  21162  dchrisum0lem2  21165  2vmadivsumlem  21187  chpdifbndlem1  21200  selberg3lem1  21204  selberg4lem1  21207  pntrsumbnd2  21214  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntibndlem2  21238  pntibndlem3  21239  pntlemn  21247  pntlemj  21250  pntlemi  21251  pntlemo  21254  pntlem3  21256  pntlemp  21257  pntleml  21258  ostth2lem1  21265  ostth2lem2  21281  ostth3  21285  usgraedgleord  21366  nbgrassovt  21400  nbgraf1o0  21409  cusgraexg  21431  cusgrafilem2  21442  cusgrafilem3  21443  sizeusglecusg  21448  1conngra  21615  vdusgraval  21631  isgrp2d  21776  opidon  21863  ghgrp  21909  rngodm1dm2  21959  zerdivemp1  21975  ubthlem1  22325  ubthlem2  22326  minvecolem3  22331  minvecolem4b  22333  minvecolem4  22335  bcsiALT  22634  occllem  22758  pjhthlem1  22846  ococin  22863  spanpr  23035  pjorthi  23124  nmbdoplbi  23480  nmcoplbi  23484  nmbdfnlbi  23505  nmcfnlbi  23508  nmopcoi  23551  branmfn  23561  hstnmoc  23679  mdsl0  23766  atomli  23838  atcvat4i  23853  atabsi  23857  abrexdomjm  23941  elpreq  23952  ifeqeqx  23954  fovcld  24003  fnct  24058  xlt2addrd  24077  supxrnemnf  24080  ssnnssfz  24101  resspos  24140  resstos  24141  ofldsqr  24193  fmcncfil  24270  xrge0iifiso  24274  elzdif0  24317  qqhval2lem  24318  esumcst  24408  esumpinfval  24416  esumpinfsum  24420  sigaclci  24468  insiga  24473  measres  24529  measdivcstOLD  24531  mbfmcnvima  24560  dya2iocnrect  24584  dya2iocnei  24585  ballotlemfp1  24702  ballotlemfrcn0  24740  lgamgulmlem5  24770  lgamcvglem  24777  derangenlem  24810  subfacp1lem3  24821  subfacp1lem5  24823  rescon  24886  cvmliftlem3  24927  cvmlift2lem10  24952  relexpadd  25091  relexpindlem  25092  rtrclreclem.trans  25099  dedekind  25140  ntrivcvgn0  25179  prodeq2ii  25192  prodmolem3  25212  fprod  25220  fprodmul  25237  fproddiv  25238  fprodm1  25243  fprod1p  25244  fprod2dlem  25257  fprodcom2  25261  wfrlem4  25473  wfrlem15  25484  frrlem4  25498  sltres  25532  nobndlem2  25561  nobndup  25568  nobnddown  25569  nofulllem3  25572  nofulllem5  25574  axlowdimlem16  25800  axlowdimlem17  25801  axcontlem3  25809  axcontlem10  25816  cgrextend  25846  segconeq  25848  trisegint  25866  ontgval  26085  wl-bitrd  26126  ftc1cnnclem  26177  ftc1cnnc  26178  ivthALT  26228  fnessref  26263  refssfne  26264  comppfsc  26277  neibastop1  26278  filnetlem4  26300  abrexdom  26322  indexdom  26326  mettrifi  26353  equivtotbnd  26377  totbndbnd  26388  prdstotbnd  26393  heibor1lem  26408  bfplem1  26421  bfplem2  26422  zerdivemp1x  26461  ofmpteq  26666  mzpsubmpt  26690  mzpsubst  26695  eqrabdioph  26726  rabdiophlem2  26752  elpell14qr2  26815  elpell1qr2  26825  pellfundre  26834  pellfundge  26835  pellfundglb  26838  pellfund14gap  26840  congabseq  26929  dvdsleabs2  26945  jm2.22  26956  jm2.23  26957  jm2.26lem3  26962  wepwsolem  27006  dnwech  27013  aomclem2  27020  aomclem4  27022  frlmup4  27121  lindff1  27158  lindfrn  27159  lmisfree  27180  dgrnznn  27208  psgnunilem4  27288  sbiota1  27502  refsumcn  27568  rfcnnnub  27574  fmul01  27577  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  cncfmptss  27584  climinf  27599  climsuselem1  27600  climsuse  27601  stoweidlem3  27619  stoweidlem16  27632  stoweidlem17  27633  stoweidlem19  27635  stoweidlem20  27636  stoweidlem23  27639  stoweidlem25  27641  stoweidlem27  27643  stoweidlem31  27647  stoweidlem34  27650  stoweidlem42  27658  stoweidlem48  27664  stoweidlem51  27667  stoweidlem52  27668  stoweidlem59  27675  wallispilem1  27681  wallispilem3  27683  stirlinglem13  27702  hashimarn  27994  swrd0swrdid  28012  swrdswrd0  28013  swrd0swrd0  28014  swrdccatin12  28026  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3  28029  usgra2wlkspth  28038  usgra2pthlem1  28040  usgra2adedgwlk  28046  usgra2adedgwlkon  28047  frgranbnb  28124  frgrancvvdeqlem3  28135  frgrancvvdeqlem9  28144  frg2woteu  28158  frg2woteqm  28162  usgreghash2spotv  28169  ordelordALT  28333  2pm13.193  28350  ee11an  28500  eel2221  28513  bnj1379  28908  bnj580  28990  bnj944  29015  bnj999  29034  bnj1204  29087  bnj1398  29109  omllaw5N  29730  cmtcomlemN  29731  cmtbr3N  29737  omlfh3N  29742  atlen0  29793  exatleN  29886  hlrelat3  29894  cvrexchlem  29901  atlelt  29920  cvrat4  29925  4atlem11b  30090  4atlem12b  30093  lneq2at  30260  cdlema1N  30273  cdlemblem  30275  paddss12  30301  paddasslem2  30303  paddasslem4  30305  paddasslem6  30307  paddasslem12  30313  paddunN  30409  poml4N  30435  poml5N  30436  osumcllem6N  30443  pexmidlem6N  30457  pl42lem2N  30462  ltrnu  30603  ltrneq2  30630  trlval2  30645  cdlemd6  30685  cdleme25b  30836  cdleme29b  30857  cdlemefr29exN  30884  ltrniotacnvval  31064  cdlemk28-3  31390  dochexmidlem7  31949
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator