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

Theorem syl31anc 1230
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 1175 . 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 972
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 974
This theorem is referenced by:  syl32anc  1235  stoic4b  1596  elovmpt3rab1  6517  smo11  7033  omeulem2  7230  oeeui  7249  oaabs2  7292  omabs  7294  omxpenlem  7616  map2xp  7685  mapdom2  7686  fsuppsssupp  7843  cantnflt  8089  cantnfltOLD  8119  cnfcom  8142  cnfcomOLD  8150  mapcdaen  8562  pwsdompw  8582  cofsmo  8647  fin1a2lem4  8781  ltmul12a  10399  lt2msq1  10429  ledivp1  10448  lemul1ad  10486  lemul2ad  10487  supmul1  10509  supmul  10512  rpnnen1lem3  11214  rpnnen1lem5  11216  lediv2ad  11282  xaddge0  11454  xadddi  11491  xadddi2  11493  supicc  11672  supiccub  11673  supicclub  11674  difelfznle  11792  flval3  11925  modidmul0  11996  fseqsupubi  12062  expcan  12192  ltexp2  12193  ltexp2r  12196  expubnd  12200  ltexp2rd  12308  ltexp2d  12313  leexp2d  12314  expcand  12315  swrdid  12626  swrd0fv  12640  swrds1  12650  ccatswrd  12655  swrdccat2  12657  swrdccatin2  12686  swrdccatin12lem2  12688  swrdccatin12lem3  12689  splfv1  12705  cshwidxmod  12748  o1fsum  13601  mertenslem1  13667  eftlub  13716  rpnnen2lem4  13823  ruclem12  13846  dvdsadd  13896  3dvds  13922  divalgmod  13936  bitsmod  13958  bitsinv1lem  13963  bezoutlem4  14051  gcdeq  14062  rplpwr  14066  sqgcd  14068  rpmulgcd2  14118  isprm5  14125  divgcdodd  14132  rpdvds  14137  divnumden  14153  crt  14180  phimullem  14181  modprm0  14202  modprmn0modprm0  14204  coprimeprodsq2  14206  pythagtriplem19  14229  pockthlem  14295  prmunb  14304  prmreclem3  14308  prmreclem6  14311  ramub  14403  ramz  14415  pmtrprfv  16347  pmtrprfv3  16348  mndodcong  16435  odngen  16466  pgpfi  16494  pgpssslw  16503  sylow2blem3  16511  lsmless1  16548  lsmless2  16549  lsmless12  16550  lsmmod2  16563  pj1id  16586  odadd2  16724  gexexlem  16727  ablfacrplem  16984  ablfacrp  16985  ablfac1b  16989  ablfac1eu  16992  pgpfac1lem2  16994  kerf1hrm  17260  lsmssspx  17602  lspsncv0  17660  coe1subfv  18175  coe1fzgsumdlem  18211  znunit  18469  uvcvvcl2  18686  uvcvv1  18687  uvcvv0  18688  scmate  18879  mdetunilem2  18982  pmatcoe1fsupp  19069  mat2pmatlin  19103  decpmatmullem  19139  pmatcollpw1lem1  19142  pmatcollpw1lem2  19143  pm2mpghm  19184  chpscmat  19210  chp0mat  19214  chpidmat  19215  cpmadugsumlemB  19242  cpmadugsumlemC  19243  cpmadugsumlemF  19244  clsndisj  19442  neiptopnei  19499  rnelfm  20320  fmfnfmlem2  20322  fmfnfm  20325  flimss1  20340  isfcf  20401  cnextfun  20430  cnextfvval  20431  cnextf  20432  cnextcn  20433  cnextfres  20434  ustuqtop1  20610  utopsnneiplem  20616  xblss2ps  20770  xblss2  20771  stdbdxmet  20884  metcnpi3  20915  metustexhalfOLD  20932  metustexhalf  20933  nmoi  21101  nmoi2  21103  nmoco  21110  blcvx  21169  icccmplem2  21194  icccmplem3  21195  reconnlem2  21198  xrge0gsumle  21204  metds0  21220  metdstri  21221  metdseq0  21224  lebnumlem3  21329  nmoleub2lem  21463  bcthlem5  21633  minveclem2  21707  minveclem3b  21709  minveclem4  21713  minveclem6  21715  icombl  21840  cncombf  21931  mbflimsup  21939  itg2monolem1  22023  itg2mono  22026  itg2cnlem1  22034  itg2cnlem2  22035  bddmulibl  22111  ellimc2  22147  cpnord  22204  cpnres  22206  dvmulbr  22208  dvcobr  22215  dvlipcn  22261  dvlip2  22262  c1liplem1  22263  dvivthlem1  22275  lhop1lem  22280  lhop1  22281  dvfsumlem2  22294  itgsubstlem  22315  deg1add  22370  deg1sublt  22377  ply1remlem  22429  plyeq0lem  22473  taylthlem2  22634  ulmdvlem3  22662  abelthlem7  22698  pilem2  22712  pilem3  22713  pige3  22775  logccv  22909  cxpaddlelem  22990  cvxcl  23179  fsumharmonic  23206  ftalem5  23215  dvdsdivcl  23322  dvdsmulf1o  23335  bposlem1  23424  lgsqr  23486  lgsquad2lem2  23499  2sqlem8a  23511  2sqlem8  23512  dchrmusum2  23544  dchrvmasumiflem1  23551  dchrisum0flblem1  23558  dchrisum0lem1b  23565  pntlem3  23659  tgdim01  23763  axsegcon  24095  ax5seglem1  24096  ax5seglem2  24097  axlowdimlem6  24115  axeuclidlem  24130  axcontlem7  24138  axcontlem9  24140  axcontlem10  24141  cusgrasize2inds  24342  usgra2adedgspth  24478  vdgrun  24766  vdgrfiun  24767  vdgr1d  24768  vdgr1b  24769  vdgr1a  24771  2pthfrgra  24876  vdn1frgrav2  24890  vdgn1frgrav2  24891  frgrawopreg  24914  frrusgraord  24936  numclwwlk2lem1  24967  numclwwlk3  24974  frgrareg  24982  nmoub3i  25553  ubthlem3  25653  minvecolem2  25656  minvecolem4  25661  minvecolem5  25662  minvecolem6  25663  htthlem  25699  pjpjpre  26202  chscllem1  26420  chscllem2  26421  chscllem3  26422  cnlnadjlem2  26852  leopnmid  26922  br8d  27328  ogrpaddlt  27574  archirngz  27599  ornglmullt  27663  orngrmullt  27664  elrhmunit  27676  qqhval2lem  27828  qqhnm  27837  qqhucn  27839  esumcst  27937  esumpcvgval  27950  measunl  28053  dya2iocbrsiga  28112  dya2icobrsiga  28113  sibfof  28148  oddpwdc  28159  eulerpartlemgc  28167  bayesth  28244  erdszelem8  28508  br8  29153  supaddc  30009  supadd  30010  totbndbnd  30253  prdsbnd  30257  rrncmslem  30296  rrntotbnd  30300  isdrngo2  30329  mzpsubst  30649  rencldnfi  30723  irrapx1  30732  pellexlem3  30735  pellexlem5  30737  infmrgelbi  30782  pellqrex  30783  pellfundge  30786  rmspecfund  30813  congtr  30871  acongeq  30889  bezoutr  30891  jm2.20nn  30907  jm2.25lem1  30908  jm2.26  30912  expdiophlem1  30931  hbtlem2  31041  suprnmpt  31397  upbdrech  31450  ssfiunibd  31454  iccintsng  31495  limcrecl  31539  dvmulcncf  31622  dvdivcncf  31624  dvbdfbdioolem1  31625  ioodvbdlimc1lem2  31629  ioodvbdlimc2lem  31631  stoweidlem1  31668  stoweidlem20  31687  stoweidlem24  31691  stoweidlem34  31701  stoweidlem45  31712  stoweidlem60  31727  fourierdlem20  31794  fourierdlem31  31805  fourierdlem38  31812  fourierdlem64  31838  fourierdlem79  31853  fourierdlem94  31868  fourierdlem113  31887  fouriersw  31899  fouriercn  31900  lincresunit3  32792  lsatcmp  34430  lcvexchlem2  34462  lcvexchlem3  34463  ncvr1  34699  cvrletrN  34700  cvrnbtwn3  34703  cvrnrefN  34709  cvrcmp  34710  0ltat  34718  atnle0  34736  atlen0  34737  cvlcvr1  34766  cvrval3  34839  atle  34862  athgt  34882  1cvratex  34899  ps-2  34904  ps-2b  34908  llnnleat  34939  2atneat  34941  llnle  34944  atcvrlln  34946  llncmp  34948  2llnmat  34950  2at0mat0  34951  2atm  34953  ps-2c  34954  lplnle  34966  lplnnle2at  34967  llncvrlpln2  34983  llncvrlpln  34984  2lplnmN  34985  2llnmj  34986  2atmat  34987  lplncmp  34988  lplnexllnN  34990  2llnm2N  34994  2llnm4  34996  lvolnle3at  35008  4atlem3a  35023  4atlem3b  35024  4atlem10  35032  4atlem11  35035  4atlem12  35038  lplncvrlvol2  35041  lplncvrlvol  35042  lvolcmp  35043  2lplnm2N  35047  2lplnmj  35048  dalempjsen  35079  dalemcea  35086  dalem2  35087  dalemdea  35088  dalem9  35098  dalem16  35105  dalemcjden  35118  dalem21  35120  dalem23  35122  dalem39  35137  dalem54  35152  dalem60  35158  cdlemb  35220  elpadd2at  35232  paddasslem4  35249  paddasslem7  35252  paddasslem15  35260  paddasslem16  35261  pmodlem1  35272  pmodlem2  35273  llnexchb2  35295  pclfinclN  35376  osumcllem9N  35390  pmapojoinN  35394  pexmidN  35395  pl42lem1N  35405  lhp0lt  35429  lhpexle1  35434  lhpexle2lem  35435  lhpexle3lem  35437  lhprelat3N  35466  ltrnid  35561  trlval3  35614  arglem1N  35617  cdlemc5  35622  cdleme3b  35656  cdleme3c  35657  cdleme3h  35662  cdleme7e  35674  cdleme7ga  35675  cdleme20l1  35748  cdleme20l2  35749  cdleme20l  35750  cdleme22b  35769  cdlemefrs29clN  35827  cdlemefrs32fva  35828  cdlemeg46fvcl  35934  cdlemeg46c  35941  cdlemeg46fvaw  35944  cdlemeg46req  35957  cdleme48fgv  35966  cdlemf1  35989  cdlemg1cex  36016  cdlemg2dN  36018  cdlemg2ce  36020  cdlemg12e  36075  cdlemg35  36141  cdlemh  36245  tendocan  36252  cdlemk28-3  36336  tendoex  36403  dih1  36715  dihmeetlem9N  36744  dihlspsnssN  36761  dihlspsnat  36762  lcfrlem23  36994  suprubd  37581  suprleubrd  37588  suprlubrd  37592
  Copyright terms: Public domain W3C validator