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

Theorem syl31anc 1231
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 1176 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 661 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  syl32anc  1236  thema4b  1595  elovmpt3rab1  6518  smo11  7032  omeulem2  7229  oeeui  7248  oaabs2  7291  omabs  7293  omxpenlem  7615  map2xp  7684  mapdom2  7685  fsuppsssupp  7841  cantnflt  8087  cantnfltOLD  8117  cnfcom  8140  cnfcomOLD  8148  mapcdaen  8560  pwsdompw  8580  cofsmo  8645  fin1a2lem4  8779  ltmul12a  10394  lt2msq1  10424  ledivp1  10443  lemul1ad  10481  lemul2ad  10482  supmul1  10504  supmul  10507  rpnnen1lem3  11206  rpnnen1lem5  11208  lediv2ad  11274  xaddge0  11446  xadddi  11483  xadddi2  11485  supicc  11664  supiccub  11665  supicclub  11666  difelfznle  11782  flval3  11915  modidmul0  11986  fseqsupubi  12052  expcan  12182  ltexp2  12183  ltexp2r  12186  expubnd  12190  ltexp2rd  12298  ltexp2d  12303  leexp2d  12304  expcand  12305  swrdid  12611  swrd0fv  12625  swrds1  12635  ccatswrd  12640  swrdccat2  12642  swrdccatin2  12671  swrdccatin12lem2  12673  swrdccatin12lem3  12674  splfv1  12690  cshwidxmod  12733  o1fsum  13586  mertenslem1  13652  eftlub  13701  rpnnen2lem4  13808  ruclem12  13831  dvdsadd  13879  3dvds  13905  divalgmod  13919  bitsmod  13941  bitsinv1lem  13946  bezoutlem4  14034  gcdeq  14045  rplpwr  14049  sqgcd  14051  rpmulgcd2  14101  isprm5  14108  divgcdodd  14115  rpdvds  14120  divnumden  14136  crt  14163  phimullem  14164  modprm0  14185  modprmn0modprm0  14187  coprimeprodsq2  14189  pythagtriplem19  14212  pockthlem  14278  prmunb  14287  prmreclem3  14291  prmreclem6  14294  ramub  14386  ramz  14398  pmtrprfv  16274  pmtrprfv3  16275  mndodcong  16362  odngen  16393  pgpfi  16421  pgpssslw  16430  sylow2blem3  16438  lsmless1  16475  lsmless2  16476  lsmless12  16477  lsmmod2  16490  pj1id  16513  odadd2  16648  gexexlem  16651  ablfacrplem  16906  ablfacrp  16907  ablfac1b  16911  ablfac1eu  16914  pgpfac1lem2  16916  kerf1hrm  17175  lsmssspx  17517  lspsncv0  17575  coe1subfv  18078  coe1fzgsumdlem  18114  znunit  18369  uvcvvcl2  18586  uvcvv1  18587  uvcvv0  18588  scmate  18779  mdetunilem2  18882  pmatcoe1fsupp  18969  mat2pmatlin  19003  decpmatmullem  19039  pmatcollpw1lem1  19042  pmatcollpw1lem2  19043  pm2mpghm  19084  chpscmat  19110  chp0mat  19114  chpidmat  19115  cpmadugsumlemB  19142  cpmadugsumlemC  19143  cpmadugsumlemF  19144  clsndisj  19342  neiptopnei  19399  rnelfm  20189  fmfnfmlem2  20191  fmfnfm  20194  flimss1  20209  isfcf  20270  cnextfun  20299  cnextfvval  20300  cnextf  20301  cnextcn  20302  cnextfres  20303  ustuqtop1  20479  utopsnneiplem  20485  xblss2ps  20639  xblss2  20640  stdbdxmet  20753  metcnpi3  20784  metustexhalfOLD  20801  metustexhalf  20802  nmoi  20970  nmoi2  20972  nmoco  20979  blcvx  21038  icccmplem2  21063  icccmplem3  21064  reconnlem2  21067  xrge0gsumle  21073  metds0  21089  metdstri  21090  metdseq0  21093  lebnumlem3  21198  nmoleub2lem  21332  bcthlem5  21502  minveclem2  21576  minveclem3b  21578  minveclem4  21582  minveclem6  21584  icombl  21709  cncombf  21800  mbflimsup  21808  itg2monolem1  21892  itg2mono  21895  itg2cnlem1  21903  itg2cnlem2  21904  bddmulibl  21980  ellimc2  22016  cpnord  22073  cpnres  22075  dvmulbr  22077  dvcobr  22084  dvlipcn  22130  dvlip2  22131  c1liplem1  22132  dvivthlem1  22144  lhop1lem  22149  lhop1  22150  dvfsumlem2  22163  itgsubstlem  22184  deg1add  22239  deg1sublt  22246  ply1remlem  22298  plyeq0lem  22342  taylthlem2  22503  ulmdvlem3  22531  abelthlem7  22567  pilem2  22581  pilem3  22582  pige3  22643  logccv  22772  cxpaddlelem  22853  cvxcl  23042  fsumharmonic  23069  ftalem5  23078  dvdsdivcl  23185  dvdsmulf1o  23198  bposlem1  23287  lgsqr  23349  lgsquad2lem2  23362  2sqlem8a  23374  2sqlem8  23375  dchrmusum2  23407  dchrvmasumiflem1  23414  dchrisum0flblem1  23421  dchrisum0lem1b  23428  pntlem3  23522  tgdim01  23626  axsegcon  23906  ax5seglem1  23907  ax5seglem2  23908  axlowdimlem6  23926  axeuclidlem  23941  axcontlem7  23949  axcontlem9  23951  axcontlem10  23952  cusgrasize2inds  24153  usgra2adedgspth  24289  vdgrun  24577  vdgrfiun  24578  vdgr1d  24579  vdgr1b  24580  vdgr1a  24582  2pthfrgra  24687  vdn1frgrav2  24702  vdgn1frgrav2  24703  frgrawopreg  24726  frrusgraord  24748  numclwwlk2lem1  24779  numclwwlk3  24786  frgrareg  24794  nmoub3i  25364  ubthlem3  25464  minvecolem2  25467  minvecolem4  25472  minvecolem5  25473  minvecolem6  25474  htthlem  25510  pjpjpre  26013  chscllem1  26231  chscllem2  26232  chscllem3  26233  cnlnadjlem2  26663  leopnmid  26733  br8d  27136  ogrpaddlt  27370  archirngz  27395  ornglmullt  27460  orngrmullt  27461  elrhmunit  27473  qqhval2lem  27598  qqhnm  27607  qqhucn  27609  esumcst  27711  esumpcvgval  27724  measunl  27827  dya2iocbrsiga  27886  dya2icobrsiga  27887  sibfof  27922  oddpwdc  27933  eulerpartlemgc  27941  bayesth  28018  erdszelem8  28282  br8  28762  supaddc  29618  supadd  29619  totbndbnd  29888  prdsbnd  29892  rrncmslem  29931  rrntotbnd  29935  isdrngo2  29964  mzpsubst  30285  rencldnfi  30359  irrapx1  30368  pellexlem3  30371  pellexlem5  30373  infmrgelbi  30418  pellqrex  30419  pellfundge  30422  rmspecfund  30449  congtr  30507  acongeq  30525  bezoutr  30527  jm2.20nn  30543  jm2.25lem1  30544  jm2.26  30548  expdiophlem1  30567  hbtlem2  30677  suprnmpt  31029  upbdrech  31082  ssfiunibd  31086  dvmulcncf  31255  dvdivcncf  31257  dvbdfbdioolem1  31258  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  stoweidlem1  31301  stoweidlem20  31320  stoweidlem24  31324  stoweidlem34  31334  stoweidlem45  31345  stoweidlem60  31360  fourierdlem20  31427  fourierdlem31  31438  fourierdlem38  31445  fourierdlem64  31471  fourierdlem79  31486  fourierdlem94  31501  fourierdlem113  31520  fouriersw  31532  fouriercn  31533  lincresunit3  32155  lsatcmp  33800  lcvexchlem2  33832  lcvexchlem3  33833  ncvr1  34069  cvrletrN  34070  cvrnbtwn3  34073  cvrnrefN  34079  cvrcmp  34080  0ltat  34088  atnle0  34106  atlen0  34107  cvlcvr1  34136  cvrval3  34209  atle  34232  athgt  34252  1cvratex  34269  ps-2  34274  ps-2b  34278  llnnleat  34309  2atneat  34311  llnle  34314  atcvrlln  34316  llncmp  34318  2llnmat  34320  2at0mat0  34321  2atm  34323  ps-2c  34324  lplnle  34336  lplnnle2at  34337  llncvrlpln2  34353  llncvrlpln  34354  2lplnmN  34355  2llnmj  34356  2atmat  34357  lplncmp  34358  lplnexllnN  34360  2llnm2N  34364  2llnm4  34366  lvolnle3at  34378  4atlem3a  34393  4atlem3b  34394  4atlem10  34402  4atlem11  34405  4atlem12  34408  lplncvrlvol2  34411  lplncvrlvol  34412  lvolcmp  34413  2lplnm2N  34417  2lplnmj  34418  dalempjsen  34449  dalemcea  34456  dalem2  34457  dalemdea  34458  dalem9  34468  dalem16  34475  dalemcjden  34488  dalem21  34490  dalem23  34492  dalem39  34507  dalem54  34522  dalem60  34528  cdlemb  34590  elpadd2at  34602  paddasslem4  34619  paddasslem7  34622  paddasslem15  34630  paddasslem16  34631  pmodlem1  34642  pmodlem2  34643  llnexchb2  34665  pclfinclN  34746  osumcllem9N  34760  pmapojoinN  34764  pexmidN  34765  pl42lem1N  34775  lhp0lt  34799  lhpexle1  34804  lhpexle2lem  34805  lhpexle3lem  34807  lhprelat3N  34836  ltrnid  34931  trlval3  34983  arglem1N  34986  cdlemc5  34991  cdleme3b  35025  cdleme3c  35026  cdleme3h  35031  cdleme7e  35043  cdleme7ga  35044  cdleme20l1  35116  cdleme20l2  35117  cdleme20l  35118  cdleme22b  35137  cdlemefrs29clN  35195  cdlemefrs32fva  35196  cdlemeg46fvcl  35302  cdlemeg46c  35309  cdlemeg46fvaw  35312  cdlemeg46req  35325  cdleme48fgv  35334  cdlemf1  35357  cdlemg1cex  35384  cdlemg2dN  35386  cdlemg2ce  35388  cdlemg12e  35443  cdlemg35  35509  cdlemh  35613  tendocan  35620  cdlemk28-3  35704  tendoex  35771  dih1  36083  dihmeetlem9N  36112  dihlspsnssN  36129  dihlspsnat  36130  lcfrlem23  36362
  Copyright terms: Public domain W3C validator