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  1849  ax13fromc9  2205  equid1  2207  elex2  2979  elex22  2980  spcimdv  3049  spsbcd  3195  disjxiun  4284  reusv2lem3  4490  opth  4561  euotd  4587  wereu  4711  wereu2  4712  tz7.7  4740  unielrel  5357  funmo  5429  iinpreima  5828  fnfvima  5950  fliftfun  6000  fliftval  6004  weniso  6040  knatar  6043  riota5f  6072  riotass2  6074  grprinvlem  6296  grprinvd  6297  ofmpteq  6333  caofref  6341  ssorduni  6392  suceloni  6419  nlimsucg  6448  tfisi  6464  zfrep6  6540  curry1  6659  curry2  6662  fnwelem  6682  funsssuppss  6710  smogt  6820  tfrlem1  6827  tfrlem5  6831  omeulem1  7013  oeworde  7024  oelimcl  7031  oeeulem  7032  oeeui  7033  nnawordex  7068  oaabs2  7076  ertr  7108  swoso  7124  qliftlem  7173  th3q  7201  resixp  7290  f1dom2g  7319  dom3d  7343  undom  7391  xpdom3  7401  domunsncan  7403  omxpenlem  7404  disjenex  7461  domssex2  7463  domssex  7464  xpf1o  7465  mapdom3  7475  findcard  7543  fiin  7664  marypha1lem  7675  marypha1  7676  fisupcl  7709  ordiso2  7721  ordtypelem2  7725  ordtypelem6  7729  ordtypelem7  7730  ordtypelem8  7731  wemapso2OLD  7758  wemapso2lem  7759  brwdom2  7780  unxpwdom2  7795  noinfepOLD  7858  cantnflt  7872  cantnfrescl  7876  oemapvali  7884  cantnflem1d  7888  cantnfltOLD  7902  cantnflem1dOLD  7911  wemapwe  7920  wemapweOLD  7921  cnfcom  7925  cnfcomOLD  7933  rankr1id  8061  tcrank  8083  cardmin2  8160  infxpenlem  8172  infxpenc2lem2  8178  infxpenc2lem2OLD  8182  fseqen  8189  dfac8clem  8194  ween  8197  ac5num  8198  indcardi  8203  acni  8207  acni2  8208  acnlem  8210  fodomfi2  8222  infpwfien  8224  inffien  8225  finnisoeu  8275  iunfictbso  8276  acacni  8301  dfac12lem2  8305  infpss  8378  infmap2  8379  ackbij1lem18  8398  ackbij1b  8400  fictb  8406  cfslb2n  8429  cofsmo  8430  cfsmolem  8431  coftr  8434  fin1ai  8454  fin2i  8456  infpssrlem4  8467  domfin4  8472  fin2i2  8479  isfin2-2  8480  fincssdom  8484  ssfin3ds  8491  fin23lem20  8498  fin23lem30  8503  isf32lem3  8516  fin1a2lem12  8572  fin1a2lem13  8573  hsmexlem2  8588  hsmexlem4  8590  axdc2lem  8609  axdc4lem  8616  ac6num  8640  ttukeylem6  8675  axdclem2  8681  imadomg  8693  iundom2g  8696  iundomg  8697  iundom  8698  unirnfdomd  8723  konigthlem  8724  iunctb  8730  fpwwe2  8802  canth4  8806  canthwelem  8809  pwfseqlem3  8819  pwfseqlem5  8822  winalim2  8855  wununi  8865  wunpw  8866  wunelss  8867  r1wunlim  8896  wunex2  8897  tsksdom  8915  tskinf  8928  inttsk  8933  inar1  8934  tskcard  8940  tskurn  8948  gruina  8977  grur1a  8978  grur1  8979  dedekind  9525  lemul12a  10179  lemulge11  10183  lediv12a  10217  nngt0  10343  peano5uzi  10722  nn0ind-raph  10734  zsupss  10936  suprzub  10938  uzsupss  10939  uzwo3  10940  rpge0  10995  fz0fzelfz0  11478  fz0fzdiffz0  11481  elfzodifsumelfzo  11596  fzonfzoufzol  11620  flltdivnn0lt  11669  fldiv  11691  modaddmodup  11754  uzrdgsuci  11775  fzennn  11782  uzindi  11795  seqcl2  11816  seqcl  11818  seqf  11819  seqfveq2  11820  seqfveq  11822  seqshft2  11824  monoord  11828  monoord2  11829  sermono  11830  seqsplit  11831  seqcaopr3  11833  seqid  11843  seqid2  11844  seqhomo  11845  seqz  11846  expcl2lem  11869  leexp1a  11914  modexp  11991  discr1  11992  discr  11993  faclbnd  12058  faclbnd6  12067  facavg  12069  hashginv  12099  hashf1rn  12115  hashge2el2dif  12176  hashimarn  12192  hashbclem  12197  fz1isolem  12206  seqcoll  12208  wrdsymb0  12251  wrdlenge2n0  12253  lsw0  12259  ccatsymb  12273  swrdvalodm2  12325  swrdvalodm  12326  swrdswrd0  12348  swrd0swrd0  12349  wrd2ind  12364  swrdccatin12  12374  swrdccat3  12375  swrdccat  12376  swrdccatid  12380  swrdccatin1d  12382  swrdccatin12d  12384  repswswrd  12414  cshwidxmod  12432  s2f1o  12518  f1oun2prg  12519  resqrex  12732  cau3lem  12834  limsupgre  12951  climi  12980  rlimi  12983  rlimclim  13016  climrlim2  13017  rlimcld2  13048  rlimcn1  13058  climcn1  13061  climcn2  13062  isercoll  13137  isercoll2  13138  climsup  13139  caucvgrlem  13142  caurcvgr  13143  iseraltlem2  13152  iseraltlem3  13153  sumeq2ii  13162  summolem3  13183  zsum  13187  fsum  13189  fsumadd  13207  fsumm1  13212  fsum1p  13214  fsum2dlem  13229  fsumcom2  13233  fsum0diag2  13242  fsummulc2  13243  fsumge1  13252  fsumabs  13256  fsumtscopo  13257  fsumtscopo2  13258  fsumparts  13261  fsumrelem  13262  fsumrlim  13266  fsumo1  13267  o1fsum  13268  fsumiun  13276  qshash  13282  isum1p  13296  isumrpcl  13298  climcndslem1  13304  climcndslem2  13305  climcnds  13306  cvgrat  13335  mertenslem1  13336  mertens  13338  sin01gt0  13466  sin02gt0  13468  efieq1re  13475  divalglem9  13597  smupvallem  13671  rppwr  13733  algfx  13747  eucalgcvga  13753  prmind2  13766  qredeq  13784  modprm0  13865  pythagtriplem4  13878  pythagtriplem6  13880  pythagtriplem7  13881  pythagtriplem12  13885  pythagtriplem13  13886  pythagtriplem14  13887  pythagtriplem16  13889  pcmpt  13946  pcmpt2  13947  prmpwdvds  13957  prmreclem2  13970  prmreclem4  13972  prmreclem5  13973  4sqlem11  14008  vdwlem1  14034  vdwlem2  14035  vdwlem9  14042  vdwlem10  14043  vdwlem11  14044  vdwlem12  14045  rami  14068  0ram  14073  0ram2  14074  0ramcl  14076  ramcl  14082  cshwsidrepsw  14112  cshwshashlem2  14115  prmlem1  14127  prmlem2  14139  strfvd  14197  strfv2d  14198  strssd  14202  firest  14363  prdsdsval3  14415  imasbas  14442  imasds  14443  imasaddfnlem  14458  imasaddvallem  14459  imasvscafn  14467  divsaddvallem  14481  divsaddflem  14482  divsaddval  14483  divsaddf  14484  divsmulval  14485  divsmulf  14486  isacs1i  14587  mreacs  14588  catidex  14604  catideu  14605  iscatd2  14611  catlid  14613  catrid  14614  subcidcl  14746  funcid  14772  invfuc  14876  yonedalem4c  15079  yonffthlem  15084  mod2ile  15268  lubss  15283  acsmapd  15340  mrcmndind  15485  gsumval2a  15503  grpidd2  15566  mulgnegnn  15628  mulgsubcl  15632  divsgrp2  15664  issubg4  15691  ghmf1  15766  pgrpsubgsymg  15904  fvcosymgeq  15925  gsmsymgreqlem1  15926  psgnunilem4  15994  pgpssslw  16104  sylow2alem2  16108  fislw  16115  efgsdmi  16220  efgsrel  16222  efgsres  16226  gexexlem  16325  gsumval3OLD  16373  gsumval3lem2  16375  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsummhm2  16424  gsummhm2OLD  16425  gsum2d  16451  gsum2dOLD  16452  dprddomcld  16471  dprdcntz  16480  dprddisj  16481  dprdss  16514  dprd2dlem2  16527  dprd2da  16529  dpjrid  16549  ablfac1eu  16562  pgpfac1lem1  16563  ablfac2  16578  srgi  16601  rngi  16645  divsrng2  16700  issrngd  16924  lssintcl  17022  islbs2  17212  lbsextlem3  17218  lbsextlem4  17219  mplsubglem  17487  mpllsslem  17488  mplsubglemOLD  17489  mpllsslemOLD  17490  subrgasclcl  17556  evlslem3  17575  evlseu  17577  mpfpf1  17760  pf1mpf  17761  zringlpirlem3  17880  zlpirlem3  17885  psgnodpm  17993  psgndiflemB  18005  frlmphl  18181  frlmup4  18204  lindff1  18224  lindfrn  18225  lmisfree  18246  mdetralt  18389  mdetunilem9  18401  slesolinv  18461  cramerimp  18467  eltg3  18542  cctop  18585  subbascn  18833  iscncl  18848  cnss2  18856  cnrmi  18939  cmpcov  18967  cmpcovf  18969  fiuncmp  18982  2ndcctbss  19034  2ndcomap  19037  2ndcsep  19038  1stcelcls  19040  islly2  19063  ptpjpre1  19119  elptr  19121  ptbasfi  19129  ptpjopn  19160  ptclsg  19163  dfac14  19166  txcnp  19168  ptcnplem  19169  uptx  19173  txtube  19188  tx2ndc  19199  xkococnlem  19207  cnmpt11  19211  cnmpt21  19219  cnmptkp  19228  cnmptk1p  19233  elqtop  19245  qtoprest  19265  qtopomap  19266  qtopcmap  19267  indishmph  19346  ptcmpfi  19361  kqhmph  19367  csdfil  19442  filssufilg  19459  ufilen  19478  rnelfm  19501  fmfnfmlem4  19505  flimcf  19530  fclscf  19573  alexsubALTlem4  19597  ptcmplem3  19601  ptcmplem4  19602  cnextfvval  19612  cnextcn  19614  tmdgsum2  19642  tsmsxplem2  19703  ucnima  19831  ucncn  19835  imasdsf1olem  19923  imasf1oxmet  19925  metss  20058  comet  20063  met2ndci  20072  prdsxmslem2  20079  metustOLD  20117  metust  20118  cfilucfilOLD  20119  cfilucfil  20120  metutopOLD  20132  psmetutop  20133  opnreen  20383  rectbntr0  20384  fsumcn  20421  rescncf  20448  xrhmeo  20493  cnheiborlem  20501  cnheibor  20502  cnllycmp  20503  lebnumlem1  20508  lebnumlem3  20510  ipcau2  20724  tchcphlem1  20725  tchcphlem2  20726  lmmcvg  20747  cfilss  20756  iscmet3lem1  20777  iscmet3lem2  20778  pjthlem1  20899  pjthlem2  20900  ivthlem1  20910  ivthlem2  20911  ivthlem3  20912  ivth2  20914  ivthle  20915  ivthle2  20916  ivthicc  20917  ovolsslem  20942  ovoliunlem1  20960  ovoliunlem2  20961  ovoliunnul  20965  ovolshftlem1  20967  ovolscalem1  20971  ovolicc2lem3  20977  ovolicc2lem4  20978  voliunlem3  21008  volsup  21012  uniiccdif  21033  uniioombllem2  21038  dyadmbl  21055  volivth  21062  vitalilem3  21065  ismbf3d  21107  mbfimaopnlem  21108  cncombf  21111  mbflimsup  21119  i1fd  21134  itg1addlem4  21152  itg2addlem  21211  itg2gt0  21213  iblitg  21221  itgconst  21271  itgfsum  21279  limcvallem  21321  cnlimci  21339  cnmptlimc  21340  limciun  21344  dvadd  21389  dvmul  21390  dvco  21396  dvrec  21404  dvcnv  21424  dvferm1lem  21431  dvferm1  21432  dvferm2lem  21433  dvferm2  21434  dvferm  21435  rollelem  21436  dvlip  21440  dvlipcn  21441  dvlip2  21442  c1liplem1  21443  c1lip2  21445  dvgt0lem1  21449  dvle  21454  dvivthlem1  21455  lhop1lem  21460  dvcnvrelem1  21464  dvcnvrelem2  21465  dvcvx  21467  dvfsumle  21468  dvfsumge  21469  dvfsumabs  21470  dvfsumlem1  21473  dvfsumlem2  21474  dvfsumlem3  21475  dvfsumlem4  21476  dvfsumrlim2  21479  dvfsum2  21481  ftc1cn  21490  ftc2ditglem  21492  itgsubstlem  21495  tdeglem4  21504  mdegaddle  21520  mdegmullem  21524  deg1sublt  21557  ply1divmo  21582  fta1g  21614  dgrub  21677  dgradd2  21710  dvply1  21725  plydivex  21738  plyrem  21746  vieta1lem2  21752  aalioulem4  21776  aalioulem5  21777  aalioulem6  21778  aaliou2  21781  taylf  21801  tayl0  21802  ulmi  21826  ulmdvlem1  21840  ulmdvlem3  21842  ulmdv  21843  mtest  21844  pserulm  21862  psercn2  21863  abelth  21881  abelth2  21882  reeff1olem  21886  efif1olem4  21976  efopn  22078  logreclem  22189  isosctrlem2  22192  rlimcnp  22334  rlimcnp2  22335  xrlimcnp  22337  scvxcvx  22354  wilthlem2  22382  basellem4  22396  ppiwordi  22475  fsumdvdscom  22500  musum  22506  musumsum  22507  chtub  22526  fsumvma  22527  chpub  22534  dchrelbas3  22552  dchrelbasd  22553  dchrn0  22564  dchrptlem2  22579  lgsval2lem  22620  lgsdirnn0  22653  lgsdinn0  22654  2sqlem6  22683  2sqlem10  22688  dchrisumlema  22712  dchrisumlem1  22713  dchrisumlem2  22714  dchrisumlem3  22715  dchrmusum2  22718  dchrvmasumlem2  22722  dchrvmasumlem3  22723  dchrvmasumiflem1  22725  dchrisum0flblem2  22733  dchrisum0flb  22734  dchrisum0re  22737  dchrisum0lem1b  22739  dchrisum0lem2  22742  2vmadivsumlem  22764  chpdifbndlem1  22777  selberg3lem1  22781  selberg4lem1  22784  pntrsumbnd2  22791  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem5  22805  pntrlog2bndlem6  22807  pntibndlem2  22815  pntibndlem3  22816  pntlemn  22824  pntlemj  22827  pntlemi  22828  pntlemo  22831  pntlem3  22833  pntlemp  22834  pntleml  22835  ostth2lem1  22842  ostth2lem2  22858  ostth3  22862  axlowdimlem16  23154  axlowdimlem17  23155  axcontlem3  23163  axcontlem10  23170  usgraedgleord  23263  nbgrassovt  23297  nbgraf1o0  23306  cusgraexg  23328  cusgrafilem2  23339  cusgrafilem3  23340  sizeusglecusg  23345  1conngra  23512  vdusgraval  23528  isgrp2d  23673  opidon  23760  ghgrp  23806  rngodm1dm2  23856  zerdivemp1  23872  ubthlem1  24222  ubthlem2  24223  minvecolem3  24228  minvecolem4b  24230  minvecolem4  24232  bcsiALT  24532  occllem  24657  pjhthlem1  24745  ococin  24762  spanpr  24934  pjorthi  25023  nmbdoplbi  25379  nmcoplbi  25383  nmbdfnlbi  25404  nmcfnlbi  25407  nmopcoi  25450  branmfn  25460  hstnmoc  25578  mdsl0  25665  atomli  25737  atcvat4i  25752  atabsi  25756  abrexdomjm  25839  elpreq  25851  ifeqeqx  25853  fovcld  25906  fnct  25964  xlt2addrd  26002  supxrnemnf  26007  ssnnssfz  26027  resspos  26071  resstos  26072  orngsqr  26223  fmcncfil  26313  xrge0iifiso  26317  elzdif0  26361  qqhval2lem  26362  esumcst  26466  esumpinfval  26474  esumpinfsum  26478  sigaclci  26527  insiga  26532  measres  26588  measdivcstOLD  26590  mbfmcnvima  26624  dya2iocnrect  26648  dya2iocnei  26649  eulerpartlemsv2  26693  eulerpartlemv  26699  eulerpartlemf  26705  eulerpartlemgh  26713  eulerpartlemgs2  26715  ballotlemfp1  26826  ballotlemfrcn0  26864  lgamgulmlem5  26971  lgamcvglem  26978  derangenlem  27011  subfacp1lem3  27022  subfacp1lem5  27024  rescon  27087  cvmliftlem3  27128  cvmlift2lem10  27153  relexpadd  27291  relexpindlem  27292  rtrclreclem.trans  27299  ntrivcvgn0  27364  prodeq2ii  27377  prodmolem3  27397  fprod  27405  fprodmul  27422  fproddiv  27423  fprodm1  27428  fprod1p  27429  fprod2dlem  27442  fprodcom2  27446  wfrlem4  27678  wfrlem15  27689  frrlem4  27722  sltres  27756  nobndlem2  27785  nobndup  27792  nobnddown  27793  nofulllem3  27796  nofulllem5  27798  cgrextend  27990  segconeq  27992  trisegint  28010  ontgval  28229  ftc1cnnclem  28418  ftc1cnnc  28419  ftc2nc  28429  dvasin  28433  dvacos  28434  ivthALT  28483  fnessref  28518  refssfne  28519  comppfsc  28532  neibastop1  28533  filnetlem4  28555  abrexdom  28577  indexdom  28581  mettrifi  28606  equivtotbnd  28630  totbndbnd  28641  prdstotbnd  28646  heibor1lem  28661  bfplem1  28674  bfplem2  28675  zerdivemp1x  28714  mzpsubmpt  29032  mzpsubst  29038  eqrabdioph  29069  rabdiophlem2  29093  elpell14qr2  29156  elpell1qr2  29166  pellfundre  29175  pellfundge  29176  pellfundglb  29179  pellfund14gap  29181  congabseq  29270  dvdsleabs2  29286  jm2.22  29297  jm2.23  29298  jm2.26lem3  29303  wepwsolem  29347  dnwech  29354  aomclem2  29361  aomclem4  29363  dgrnznn  29445  itgpowd  29543  sbiota1  29641  refsumcn  29705  rfcnnnub  29711  fmul01  29714  fmuldfeqlem1  29716  fmuldfeq  29717  fmul01lt1lem1  29718  fmul01lt1lem2  29719  cncfmptss  29721  climinf  29732  climsuselem1  29733  climsuse  29734  stoweidlem3  29751  stoweidlem16  29764  stoweidlem17  29765  stoweidlem19  29767  stoweidlem20  29768  stoweidlem23  29771  stoweidlem25  29773  stoweidlem27  29775  stoweidlem31  29779  stoweidlem34  29782  stoweidlem42  29790  stoweidlem48  29796  stoweidlem51  29799  stoweidlem52  29800  stoweidlem59  29807  wallispilem1  29813  wallispilem3  29815  stirlinglem13  29834  2leaddle2  30128  ige2m2fzo  30173  wwlktovfo  30206  wrd2f1tovbij  30208  nbgrassvwo  30229  usgra2wlkspth  30251  usgra2pthlem1  30253  usgra2adedgwlk  30259  usgra2adedgwlkon  30260  wlkiswwlk2lem3  30280  wwlkextbij  30318  wwlkexthasheq  30319  clwlkisclwwlklem0  30403  wwlksubclwwlk  30419  clwwisshclwwlem1  30422  eleclclwwlknlem1  30443  eleclclwwlknlem2  30444  Lemma2  30446  usg2cwwkdifex  30448  clwlkfclwwlk  30470  clwlkf1clwwlklem  30475  clwlksizeeq  30478  rusgranumwlkl1lem1  30511  rusgranumwlklem4  30523  rusgra0edg  30526  rusgranumwwlkg  30530  frgranbnb  30565  frgrancvvdeqlem3  30578  frgrancvvdeqlem9  30587  frg2woteu  30601  frg2woteqm  30605  usgreghash2spotv  30612  numclwwlkovf2ex  30632  numclwlk1lem2fo  30641  numclwwlkqhash  30646  numclwwlk2lem1  30648  numclwlk2lem2f  30649  numclwwlk2lem3  30652  numclwwlk5  30658  numclwwlk7  30660  ssnn0ssfz  30693  supgtoreq  30694  fsuppmapnn0fiubex  30749  mat0dimscm  30788  mdetdiagid  30826  ldepspr  30896  ordelordALT  31131  2pm13.193  31148  ee11an  31299  eel2221  31312  bnj1379  31711  bnj580  31793  bnj944  31818  bnj999  31837  bnj1204  31890  bnj1398  31912  bj-babygodel  32002  bj-finsumval0  32426  omllaw5N  32732  cmtcomlemN  32733  cmtbr3N  32739  omlfh3N  32744  atlen0  32795  exatleN  32888  hlrelat3  32896  cvrexchlem  32903  atlelt  32922  cvrat4  32927  4atlem11b  33092  4atlem12b  33095  lneq2at  33262  cdlema1N  33275  cdlemblem  33277  paddss12  33303  paddasslem2  33305  paddasslem4  33307  paddasslem6  33309  paddasslem12  33315  paddunN  33411  poml4N  33437  poml5N  33438  osumcllem6N  33445  pexmidlem6N  33459  pl42lem2N  33464  ltrnu  33605  ltrneq2  33632  trlval2  33647  cdlemd6  33687  cdleme25b  33838  cdleme29b  33859  cdlemefr29exN  33886  ltrniotacnvval  34066  cdlemk28-3  34392  dochexmidlem7  34951
  Copyright terms: Public domain W3C validator