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

Theorem syl31anc 1267
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 1185 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 665 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  syl32anc  1272  stoic4b  1656  elovmpt3rab1  6478  smo11  7031  omeulem2  7232  oeeui  7251  oaabs2  7294  omabs  7296  omxpenlem  7619  map2xp  7688  mapdom2  7689  fsuppsssupp  7845  cantnflt  8122  cnfcom  8150  mapcdaen  8558  pwsdompw  8578  cofsmo  8643  fin1a2lem4  8777  ltmul12a  10405  lt2msq1  10434  ledivp1  10452  lemul1ad  10490  lemul2ad  10491  supaddc  10518  supadd  10519  supmul1  10520  supmul  10523  rpnnen1lem3  11236  rpnnen1lem5  11238  lediv2ad  11307  xaddge0  11488  xadddi  11525  xadddi2  11527  supicc  11724  supiccub  11725  supicclub  11726  difelfznle  11849  flval3  11993  modidmul0OLD  12066  fseqsupubi  12134  expcan  12268  ltexp2  12269  ltexp2r  12272  expubnd  12276  ltexp2rd  12383  ltexp2d  12388  leexp2d  12389  expcand  12390  swrdid  12723  swrd0fv  12734  swrds1  12746  ccatswrd  12751  swrdccat2  12753  swrdccatin2  12782  swrdccatin12lem2  12784  swrdccatin12lem3  12785  splfv1  12801  cshwidxmod  12844  o1fsum  13809  mertenslem1  13876  eftlub  14099  rpnnen2lem4  14206  ruclem12  14229  dvdsadd  14279  3dvds  14305  divalgmod  14323  bitsmod  14346  bitsinv1lem  14351  bezoutlem4OLD  14442  bezoutlem4  14445  gcdeq  14456  rplpwr  14460  sqgcd  14462  isprm5  14587  divgcdodd  14589  rpmulgcd2  14598  rpdvds  14612  coprmproddvdslem  14615  divnumden  14633  crt  14662  phimullem  14663  modprm0  14692  modprmn0modprm0  14694  coprimeprodsq2  14696  pythagtriplem19  14719  pockthlem  14785  prmunb  14794  prmreclem3  14798  prmreclem6  14801  ramub  14906  ramz  14919  pmtrprfv  17030  pmtrprfv3  17031  mndodcong  17127  odngen  17162  pgpfi  17193  pgpssslw  17202  sylow2blem3  17210  lsmless1  17247  lsmless2  17248  lsmless12  17249  lsmmod2  17262  pj1id  17285  odadd2  17423  gexexlem  17426  ablfacrplem  17634  ablfacrp  17635  ablfac1b  17639  ablfac1eu  17642  pgpfac1lem2  17644  kerf1hrm  17907  lsmssspx  18247  lspsncv0  18305  coe1subfv  18795  coe1fzgsumdlem  18831  znunit  19069  uvcvvcl2  19281  uvcvv1  19282  uvcvv0  19283  scmate  19470  mdetunilem2  19573  pmatcoe1fsupp  19660  mat2pmatlin  19694  decpmatmullem  19730  pmatcollpw1lem1  19733  pmatcollpw1lem2  19734  pm2mpghm  19775  chpscmat  19801  chp0mat  19805  chpidmat  19806  cpmadugsumlemB  19833  cpmadugsumlemC  19834  cpmadugsumlemF  19835  clsndisj  20026  neiptopnei  20083  rnelfm  20903  fmfnfmlem2  20905  fmfnfm  20908  flimss1  20923  isfcf  20984  cnextfun  21014  cnextfvval  21015  cnextf  21016  cnextcn  21017  cnextfres1  21018  ustuqtop1  21191  utopsnneiplem  21197  xblss2ps  21351  xblss2  21352  stdbdxmet  21465  metcnpi3  21496  metustexhalf  21506  nmoi  21668  nmoi2  21670  nmoiOLD  21684  nmoi2OLD  21686  nmoco  21693  blcvx  21751  icccmplem2  21776  icccmplem3  21777  reconnlem2  21780  xrge0gsumle  21786  metds0  21802  metdstri  21803  metdseq0  21806  metds0OLD  21817  metdstriOLD  21818  metdseq0OLD  21821  lebnumlem3  21926  lebnumlem3OLD  21929  nmoleub2lem  22063  bcthlem5  22231  minveclem2  22303  minveclem3b  22305  minveclem4  22309  minveclem6  22311  minveclem2OLD  22315  minveclem3bOLD  22317  minveclem4OLD  22321  minveclem6OLD  22323  icombl  22452  cncombf  22549  mbflimsup  22558  mbflimsupOLD  22559  itg2monolem1  22643  itg2mono  22646  itg2cnlem1  22654  itg2cnlem2  22655  bddmulibl  22731  ellimc2  22767  cpnord  22824  cpnres  22826  dvmulbr  22828  dvcobr  22835  dvlipcn  22881  dvlip2  22882  c1liplem1  22883  dvivthlem1  22895  lhop1lem  22900  lhop1  22901  dvfsumlem2  22914  itgsubstlem  22935  deg1add  22987  deg1sublt  22994  ply1remlem  23048  plyeq0lem  23099  taylthlem2  23264  ulmdvlem3  23292  abelthlem7  23328  pilem2  23342  pilem2OLD  23343  pilem3  23344  pilem3OLD  23345  pige3  23407  logccv  23543  cxpaddlelem  23626  cvxcl  23845  fsumharmonic  23872  ftalem5  23936  ftalem5OLD  23938  dvdsdivcl  24045  dvdsmulf1o  24058  bposlem1  24147  lgsqr  24209  lgsquad2lem2  24222  2sqlem8a  24234  2sqlem8  24235  dchrmusum2  24267  dchrvmasumiflem1  24274  dchrisum0flblem1  24281  dchrisum0lem1b  24288  pntlem3  24382  tgdim01  24486  axsegcon  24892  ax5seglem1  24893  ax5seglem2  24894  axlowdimlem6  24912  axeuclidlem  24927  axcontlem7  24935  axcontlem9  24937  axcontlem10  24938  cusgrasize2inds  25140  usgra2adedgspth  25276  vdgrun  25564  vdgrfiun  25565  vdgr1d  25566  vdgr1b  25567  vdgr1a  25569  2pthfrgra  25674  vdn1frgrav2  25688  vdgn1frgrav2  25689  frgrawopreg  25712  frrusgraord  25734  numclwwlk2lem1  25765  numclwwlk3  25772  frgrareg  25780  nmoub3i  26349  ubthlem3  26449  minvecolem2  26452  minvecolem4  26457  minvecolem5  26458  minvecolem6  26459  minvecolem2OLD  26462  minvecolem4OLD  26467  minvecolem5OLD  26468  minvecolem6OLD  26469  htthlem  26505  pjpjpre  27007  chscllem1  27225  chscllem2  27226  chscllem3  27227  cnlnadjlem2  27656  leopnmid  27726  br8d  28157  ogrpaddlt  28425  archirngz  28450  ornglmullt  28515  orngrmullt  28516  elrhmunit  28528  qqhval2lem  28730  qqhnm  28739  qqhucn  28741  esumcst  28829  esumpcvgval  28844  measunl  28983  dya2iocbrsiga  29042  dya2icobrsiga  29043  omssubadd  29073  omssubaddOLD  29077  inelcarsg  29088  carsgclctunlem2  29096  sibfof  29118  sitgaddlemb  29126  oddpwdc  29132  eulerpartlemgc  29140  bayesth  29217  erdszelem8  29866  br8  30340  totbndbnd  32022  prdsbnd  32026  rrncmslem  32065  rrntotbnd  32069  isdrngo2  32098  lsatcmp  32475  lcvexchlem2  32507  lcvexchlem3  32508  ncvr1  32744  cvrletrN  32745  cvrnbtwn3  32748  cvrnrefN  32754  cvrcmp  32755  0ltat  32763  atnle0  32781  atlen0  32782  cvlcvr1  32811  cvrval3  32884  atle  32907  athgt  32927  1cvratex  32944  ps-2  32949  ps-2b  32953  llnnleat  32984  2atneat  32986  llnle  32989  atcvrlln  32991  llncmp  32993  2llnmat  32995  2at0mat0  32996  2atm  32998  ps-2c  32999  lplnle  33011  lplnnle2at  33012  llncvrlpln2  33028  llncvrlpln  33029  2lplnmN  33030  2llnmj  33031  2atmat  33032  lplncmp  33033  lplnexllnN  33035  2llnm2N  33039  2llnm4  33041  lvolnle3at  33053  4atlem3a  33068  4atlem3b  33069  4atlem10  33077  4atlem11  33080  4atlem12  33083  lplncvrlvol2  33086  lplncvrlvol  33087  lvolcmp  33088  2lplnm2N  33092  2lplnmj  33093  dalempjsen  33124  dalemcea  33131  dalem2  33132  dalemdea  33133  dalem9  33143  dalem16  33150  dalemcjden  33163  dalem21  33165  dalem23  33167  dalem39  33182  dalem54  33197  dalem60  33203  cdlemb  33265  elpadd2at  33277  paddasslem4  33294  paddasslem7  33297  paddasslem15  33305  paddasslem16  33306  pmodlem1  33317  pmodlem2  33318  llnexchb2  33340  pclfinclN  33421  osumcllem9N  33435  pmapojoinN  33439  pexmidN  33440  pl42lem1N  33450  lhp0lt  33474  lhpexle1  33479  lhpexle2lem  33480  lhpexle3lem  33482  lhprelat3N  33511  ltrnid  33606  trlval3  33659  arglem1N  33662  cdlemc5  33667  cdleme3b  33701  cdleme3c  33702  cdleme3h  33707  cdleme7e  33719  cdleme7ga  33720  cdleme20l1  33793  cdleme20l2  33794  cdleme20l  33795  cdleme22b  33814  cdlemefrs29clN  33872  cdlemefrs32fva  33873  cdlemeg46fvcl  33979  cdlemeg46c  33986  cdlemeg46fvaw  33989  cdlemeg46req  34002  cdleme48fgv  34011  cdlemf1  34034  cdlemg1cex  34061  cdlemg2dN  34063  cdlemg2ce  34065  cdlemg12e  34120  cdlemg35  34186  cdlemh  34290  tendocan  34297  cdlemk28-3  34381  tendoex  34448  dih1  34760  dihmeetlem9N  34789  dihlspsnssN  34806  dihlspsnat  34807  lcfrlem23  35039  mzpsubst  35496  rencldnfi  35570  irrapx1  35579  pellexlem3  35582  pellexlem5  35584  infmrgelbi  35631  infmrgelbiOLD  35632  pellqrex  35633  pellfundge  35637  rmspecfund  35664  congtr  35722  acongeq  35740  bezoutr  35742  jm2.20nn  35759  jm2.25lem1  35760  jm2.26  35764  expdiophlem1  35783  hbtlem2  35890  suprubd  36509  suprleubrd  36516  suprlubrd  36520  suprnmpt  37336  wessf1ornlem  37357  upbdrech  37414  ssfiunibd  37418  uzfissfz  37440  xleadd2d  37441  suprltrp  37442  xleadd1d  37443  iccintsng  37510  limcrecl  37586  dvmulcncf  37674  dvdivcncf  37676  dvbdfbdioolem1  37677  ioodvbdlimc1lem2  37681  ioodvbdlimc1lem2OLD  37683  ioodvbdlimc2lem  37685  ioodvbdlimc2lemOLD  37686  stoweidlem1  37738  stoweidlem20  37757  stoweidlem24  37761  stoweidlem34  37772  stoweidlem45  37783  stoweidlem60  37798  fourierdlem20  37866  fourierdlem31  37877  fourierdlem31OLD  37878  fourierdlem38  37885  fourierdlem64  37911  fourierdlem79  37926  fourierdlem94  37941  fourierdlem113  37960  fouriersw  37972  fouriercn  37973  sge0isum  38114  hoicvr  38211  ovnsubaddlem2  38234  hoidmv1lelem1  38254  hoidmv1lelem3  38256  hoidmvlelem1  38258  hoidmvlelem4  38261  gcdzeq  38600  pfxfv  38747  cusgrsize2inds  39236  lincresunit3  39861  elbigolo1  39955
  Copyright terms: Public domain W3C validator