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

Theorem syl31anc 1279
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
syl31anc.5  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
Assertion
Ref Expression
syl31anc  |-  ( ph  ->  et )

Proof of Theorem syl31anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1194 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 671 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993
This theorem is referenced by:  syl32anc  1284  stoic4b  1673  elovmpt3rab1  6554  smo11  7109  omeulem2  7310  oeeui  7329  oaabs2  7372  omabs  7374  omxpenlem  7699  map2xp  7768  mapdom2  7769  fsuppsssupp  7925  cantnflt  8203  cnfcom  8231  mapcdaen  8640  pwsdompw  8660  cofsmo  8725  fin1a2lem4  8859  ltmul12a  10489  lt2msq1  10518  ledivp1  10536  lemul1ad  10574  lemul2ad  10575  supaddc  10602  supadd  10603  supmul1  10604  supmul  10607  rpnnen1lem3  11321  rpnnen1lem5  11323  lediv2ad  11392  xaddge0  11573  xadddi  11610  xadddi2  11612  supicc  11809  supiccub  11810  supicclub  11811  difelfznle  11935  flval3  12082  modidmul0OLD  12155  fseqsupubi  12223  expcan  12357  ltexp2  12358  ltexp2r  12361  expubnd  12365  ltexp2rd  12472  ltexp2d  12477  leexp2d  12478  expcand  12479  swrdid  12821  swrd0fv  12832  swrds1  12844  ccatswrd  12849  swrdccat2  12851  swrdccatin2  12880  swrdccatin12lem2  12882  swrdccatin12lem3  12883  splfv1  12899  cshwidxmod  12942  o1fsum  13922  mertenslem1  13989  eftlub  14212  rpnnen2lem4  14319  ruclem12  14342  dvdsadd  14392  3dvds  14418  divalgmod  14436  bitsmod  14459  bitsinv1lem  14464  bezoutlem4OLD  14555  bezoutlem4  14558  gcdeq  14569  rplpwr  14573  sqgcd  14575  isprm5  14700  divgcdodd  14702  rpmulgcd2  14711  rpdvds  14725  coprmproddvdslem  14728  divnumden  14746  crt  14775  phimullem  14776  modprm0  14805  modprmn0modprm0  14807  coprimeprodsq2  14809  pythagtriplem19  14832  pockthlem  14898  prmunb  14907  prmreclem3  14911  prmreclem6  14914  ramub  15019  ramz  15032  pmtrprfv  17143  pmtrprfv3  17144  mndodcong  17240  odngen  17275  pgpfi  17306  pgpssslw  17315  sylow2blem3  17323  lsmless1  17360  lsmless2  17361  lsmless12  17362  lsmmod2  17375  pj1id  17398  odadd2  17536  gexexlem  17539  ablfacrplem  17747  ablfacrp  17748  ablfac1b  17752  ablfac1eu  17755  pgpfac1lem2  17757  kerf1hrm  18020  lsmssspx  18360  lspsncv0  18418  coe1subfv  18908  coe1fzgsumdlem  18944  znunit  19183  uvcvvcl2  19395  uvcvv1  19396  uvcvv0  19397  scmate  19584  mdetunilem2  19687  pmatcoe1fsupp  19774  mat2pmatlin  19808  decpmatmullem  19844  pmatcollpw1lem1  19847  pmatcollpw1lem2  19848  pm2mpghm  19889  chpscmat  19915  chp0mat  19919  chpidmat  19920  cpmadugsumlemB  19947  cpmadugsumlemC  19948  cpmadugsumlemF  19949  clsndisj  20140  neiptopnei  20197  rnelfm  21017  fmfnfmlem2  21019  fmfnfm  21022  flimss1  21037  isfcf  21098  cnextfun  21128  cnextfvval  21129  cnextf  21130  cnextcn  21131  cnextfres1  21132  ustuqtop1  21305  utopsnneiplem  21311  xblss2ps  21465  xblss2  21466  stdbdxmet  21579  metcnpi3  21610  metustexhalf  21620  nmoi  21782  nmoi2  21784  nmoiOLD  21798  nmoi2OLD  21800  nmoco  21807  blcvx  21865  icccmplem2  21890  icccmplem3  21891  reconnlem2  21894  xrge0gsumle  21900  metds0  21916  metdstri  21917  metdseq0  21920  metds0OLD  21931  metdstriOLD  21932  metdseq0OLD  21935  lebnumlem3  22040  lebnumlem3OLD  22043  nmoleub2lem  22177  bcthlem5  22345  minveclem2  22417  minveclem3b  22419  minveclem4  22423  minveclem6  22425  minveclem2OLD  22429  minveclem3bOLD  22431  minveclem4OLD  22435  minveclem6OLD  22437  icombl  22566  cncombf  22663  mbflimsup  22672  mbflimsupOLD  22673  itg2monolem1  22757  itg2mono  22760  itg2cnlem1  22768  itg2cnlem2  22769  bddmulibl  22845  ellimc2  22881  cpnord  22938  cpnres  22940  dvmulbr  22942  dvcobr  22949  dvlipcn  22995  dvlip2  22996  c1liplem1  22997  dvivthlem1  23009  lhop1lem  23014  lhop1  23015  dvfsumlem2  23028  itgsubstlem  23049  deg1add  23101  deg1sublt  23108  ply1remlem  23162  plyeq0lem  23213  taylthlem2  23378  ulmdvlem3  23406  abelthlem7  23442  pilem2  23456  pilem2OLD  23457  pilem3  23458  pilem3OLD  23459  pige3  23521  logccv  23657  cxpaddlelem  23740  cvxcl  23959  fsumharmonic  23986  ftalem5  24050  ftalem5OLD  24052  dvdsdivcl  24159  dvdsmulf1o  24172  bposlem1  24261  lgsqr  24323  lgsquad2lem2  24336  2sqlem8a  24348  2sqlem8  24349  dchrmusum2  24381  dchrvmasumiflem1  24388  dchrisum0flblem1  24395  dchrisum0lem1b  24402  pntlem3  24496  tgdim01  24600  axsegcon  25006  ax5seglem1  25007  ax5seglem2  25008  axlowdimlem6  25026  axeuclidlem  25041  axcontlem7  25049  axcontlem9  25051  axcontlem10  25052  cusgrasize2inds  25254  usgra2adedgspth  25390  vdgrun  25678  vdgrfiun  25679  vdgr1d  25680  vdgr1b  25681  vdgr1a  25683  2pthfrgra  25788  vdn1frgrav2  25802  vdgn1frgrav2  25803  frgrawopreg  25826  frrusgraord  25848  numclwwlk2lem1  25879  numclwwlk3  25886  frgrareg  25894  nmoub3i  26463  ubthlem3  26563  minvecolem2  26566  minvecolem4  26571  minvecolem5  26572  minvecolem6  26573  minvecolem2OLD  26576  minvecolem4OLD  26581  minvecolem5OLD  26582  minvecolem6OLD  26583  htthlem  26619  pjpjpre  27121  chscllem1  27339  chscllem2  27340  chscllem3  27341  cnlnadjlem2  27770  leopnmid  27840  br8d  28267  ogrpaddlt  28530  archirngz  28555  ornglmullt  28619  orngrmullt  28620  elrhmunit  28632  qqhval2lem  28834  qqhnm  28843  qqhucn  28845  esumcst  28933  esumpcvgval  28948  measunl  29087  dya2iocbrsiga  29146  dya2icobrsiga  29147  omssubadd  29177  omssubaddOLD  29181  inelcarsg  29192  carsgclctunlem2  29200  sibfof  29222  sitgaddlemb  29230  oddpwdc  29236  eulerpartlemgc  29244  bayesth  29321  erdszelem8  29970  br8  30445  totbndbnd  32166  prdsbnd  32170  rrncmslem  32209  rrntotbnd  32213  isdrngo2  32242  lsatcmp  32614  lcvexchlem2  32646  lcvexchlem3  32647  ncvr1  32883  cvrletrN  32884  cvrnbtwn3  32887  cvrnrefN  32893  cvrcmp  32894  0ltat  32902  atnle0  32920  atlen0  32921  cvlcvr1  32950  cvrval3  33023  atle  33046  athgt  33066  1cvratex  33083  ps-2  33088  ps-2b  33092  llnnleat  33123  2atneat  33125  llnle  33128  atcvrlln  33130  llncmp  33132  2llnmat  33134  2at0mat0  33135  2atm  33137  ps-2c  33138  lplnle  33150  lplnnle2at  33151  llncvrlpln2  33167  llncvrlpln  33168  2lplnmN  33169  2llnmj  33170  2atmat  33171  lplncmp  33172  lplnexllnN  33174  2llnm2N  33178  2llnm4  33180  lvolnle3at  33192  4atlem3a  33207  4atlem3b  33208  4atlem10  33216  4atlem11  33219  4atlem12  33222  lplncvrlvol2  33225  lplncvrlvol  33226  lvolcmp  33227  2lplnm2N  33231  2lplnmj  33232  dalempjsen  33263  dalemcea  33270  dalem2  33271  dalemdea  33272  dalem9  33282  dalem16  33289  dalemcjden  33302  dalem21  33304  dalem23  33306  dalem39  33321  dalem54  33336  dalem60  33342  cdlemb  33404  elpadd2at  33416  paddasslem4  33433  paddasslem7  33436  paddasslem15  33444  paddasslem16  33445  pmodlem1  33456  pmodlem2  33457  llnexchb2  33479  pclfinclN  33560  osumcllem9N  33574  pmapojoinN  33578  pexmidN  33579  pl42lem1N  33589  lhp0lt  33613  lhpexle1  33618  lhpexle2lem  33619  lhpexle3lem  33621  lhprelat3N  33650  ltrnid  33745  trlval3  33798  arglem1N  33801  cdlemc5  33806  cdleme3b  33840  cdleme3c  33841  cdleme3h  33846  cdleme7e  33858  cdleme7ga  33859  cdleme20l1  33932  cdleme20l2  33933  cdleme20l  33934  cdleme22b  33953  cdlemefrs29clN  34011  cdlemefrs32fva  34012  cdlemeg46fvcl  34118  cdlemeg46c  34125  cdlemeg46fvaw  34128  cdlemeg46req  34141  cdleme48fgv  34150  cdlemf1  34173  cdlemg1cex  34200  cdlemg2dN  34202  cdlemg2ce  34204  cdlemg12e  34259  cdlemg35  34325  cdlemh  34429  tendocan  34436  cdlemk28-3  34520  tendoex  34587  dih1  34899  dihmeetlem9N  34928  dihlspsnssN  34945  dihlspsnat  34946  lcfrlem23  35178  mzpsubst  35635  rencldnfi  35709  irrapx1  35717  pellexlem3  35720  pellexlem5  35722  infmrgelbi  35769  infmrgelbiOLD  35770  pellqrex  35771  pellfundge  35775  rmspecfund  35802  congtr  35860  acongeq  35878  bezoutr  35880  jm2.20nn  35897  jm2.25lem1  35898  jm2.26  35902  expdiophlem1  35921  hbtlem2  36028  suprubd  36647  suprleubrd  36654  suprlubrd  36658  suprnmpt  37477  wessf1ornlem  37497  mpct  37520  upbdrech  37561  ssfiunibd  37565  uzfissfz  37587  xleadd2d  37588  suprltrp  37589  xleadd1d  37590  iccintsng  37662  limcrecl  37747  dvmulcncf  37835  dvdivcncf  37837  dvbdfbdioolem1  37838  ioodvbdlimc1lem2  37842  ioodvbdlimc1lem2OLD  37844  ioodvbdlimc2lem  37846  ioodvbdlimc2lemOLD  37847  stoweidlem1  37899  stoweidlem20  37918  stoweidlem24  37922  stoweidlem34  37933  stoweidlem45  37944  stoweidlem60  37959  fourierdlem20  38027  fourierdlem31  38038  fourierdlem31OLD  38039  fourierdlem38  38046  fourierdlem64  38072  fourierdlem79  38087  fourierdlem94  38102  fourierdlem113  38121  fouriersw  38133  fouriercn  38134  sge0isum  38307  hoicvr  38408  ovnsubaddlem2  38431  hoidmv1lelem1  38451  hoidmv1lelem3  38453  hoidmvlelem1  38455  hoidmvlelem4  38458  gcdzeq  38831  pfxfv  38980  nbupgr  39462  nbumgrvtx  39464  cusgrsize2inds  39564  upgr1wlkwlk  39700  2pthnloop  39764  1pthond  39859  2trlond  39888  3trlond  39914  3pthond  39916  3spthond  39918  lincresunit3  40547  elbigolo1  40641
  Copyright terms: Public domain W3C validator