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

Theorem syl31anc 1222
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 1168 . 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 965
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 967
This theorem is referenced by:  syl32anc  1227  thema4b  1586  smo11  6936  omeulem2  7133  oeeui  7152  oaabs2  7195  omabs  7197  omxpenlem  7523  map2xp  7592  mapdom2  7593  fsuppsssupp  7748  cantnflt  7992  cantnfltOLD  8022  cnfcom  8045  cnfcomOLD  8053  mapcdaen  8465  pwsdompw  8485  cofsmo  8550  fin1a2lem4  8684  ltmul12a  10297  lt2msq1  10327  ledivp1  10346  lemul1ad  10384  lemul2ad  10385  supmul1  10407  supmul  10410  rpnnen1lem3  11093  rpnnen1lem5  11095  lediv2ad  11161  xaddge0  11333  xadddi  11370  xadddi2  11372  supicc  11551  supiccub  11552  supicclub  11553  flval3  11781  modidmul0  11852  fseqsupubi  11918  expcan  12034  ltexp2  12035  ltexp2r  12038  expubnd  12042  ltexp2rd  12150  ltexp2d  12155  leexp2d  12156  expcand  12157  swrdid  12440  swrd0fv  12454  swrds1  12464  ccatswrd  12469  swrdccat2  12471  swrdccatin2  12497  swrdccatin12lem2  12499  swrdccatin12lem3  12500  splfv1  12516  cshwidxmod  12559  o1fsum  13395  mertenslem1  13463  eftlub  13512  rpnnen2lem4  13619  ruclem12  13642  dvdsadd  13690  3dvds  13715  divalgmod  13729  bitsmod  13751  bitsinv1lem  13756  bezoutlem4  13844  gcdeq  13855  rplpwr  13859  sqgcd  13861  rpmulgcd2  13910  isprm5  13917  divgcdodd  13924  rpdvds  13929  divnumden  13945  crt  13972  phimullem  13973  modprm0  13992  modprmn0modprm0  13994  coprimeprodsq2  13996  pythagtriplem19  14019  pockthlem  14085  prmunb  14094  prmreclem3  14098  prmreclem6  14101  ramub  14193  ramz  14205  pmtrprfv  16079  pmtrprfv3  16080  mndodcong  16167  odngen  16198  pgpfi  16226  pgpssslw  16235  sylow2blem3  16243  lsmless1  16280  lsmless2  16281  lsmless12  16282  lsmmod2  16295  pj1id  16318  odadd2  16453  gexexlem  16456  ablfacrplem  16689  ablfacrp  16690  ablfac1b  16694  ablfac1eu  16697  pgpfac1lem2  16699  kerf1hrm  16955  lsmssspx  17293  lspsncv0  17351  coe1subfv  17844  znunit  18122  uvcvvcl2  18339  uvcvv1  18340  uvcvv0  18341  mdetunilem2  18552  clsndisj  18812  neiptopnei  18869  rnelfm  19659  fmfnfmlem2  19661  fmfnfm  19664  flimss1  19679  isfcf  19740  cnextfun  19769  cnextfvval  19770  cnextf  19771  cnextcn  19772  cnextfres  19773  ustuqtop1  19949  utopsnneiplem  19955  xblss2ps  20109  xblss2  20110  stdbdxmet  20223  metcnpi3  20254  metustexhalfOLD  20271  metustexhalf  20272  nmoi  20440  nmoi2  20442  nmoco  20449  blcvx  20508  icccmplem2  20533  icccmplem3  20534  reconnlem2  20537  xrge0gsumle  20543  metds0  20559  metdstri  20560  metdseq0  20563  lebnumlem3  20668  nmoleub2lem  20802  bcthlem5  20972  minveclem2  21046  minveclem3b  21048  minveclem4  21052  minveclem6  21054  icombl  21179  cncombf  21270  mbflimsup  21278  itg2monolem1  21362  itg2mono  21365  itg2cnlem1  21373  itg2cnlem2  21374  bddmulibl  21450  ellimc2  21486  cpnord  21543  cpnres  21545  dvmulbr  21547  dvcobr  21554  dvlipcn  21600  dvlip2  21601  c1liplem1  21602  dvivthlem1  21614  lhop1lem  21619  lhop1  21620  dvfsumlem2  21633  itgsubstlem  21654  deg1add  21709  deg1sublt  21716  ply1remlem  21768  plyeq0lem  21812  taylthlem2  21973  ulmdvlem3  22001  abelthlem7  22037  pilem2  22051  pilem3  22052  pige3  22113  logccv  22242  cxpaddlelem  22323  cvxcl  22512  fsumharmonic  22539  ftalem5  22548  dvdsdivcl  22655  dvdsmulf1o  22668  bposlem1  22757  lgsqr  22819  lgsquad2lem2  22832  2sqlem8a  22844  2sqlem8  22845  dchrmusum2  22877  dchrvmasumiflem1  22884  dchrisum0flblem1  22891  dchrisum0lem1b  22898  pntlem3  22992  tgdim01  23096  axsegcon  23326  ax5seglem1  23327  ax5seglem2  23328  axlowdimlem6  23346  axeuclidlem  23361  axcontlem7  23369  axcontlem9  23371  axcontlem10  23372  cusgrasize2inds  23538  vdgrun  23724  vdgrfiun  23725  vdgr1d  23726  vdgr1b  23727  vdgr1a  23729  nmoub3i  24326  ubthlem3  24426  minvecolem2  24429  minvecolem4  24434  minvecolem5  24435  minvecolem6  24436  htthlem  24472  pjpjpre  24975  chscllem1  25193  chscllem2  25194  chscllem3  25195  cnlnadjlem2  25625  leopnmid  25695  br8d  26094  ogrpaddlt  26327  archirngz  26352  ornglmullt  26421  orngrmullt  26422  elrhmunit  26434  qqhval2lem  26556  qqhnm  26565  qqhucn  26567  esumcst  26660  esumpcvgval  26673  measunl  26776  dya2iocbrsiga  26835  dya2icobrsiga  26836  sibfof  26871  oddpwdc  26882  eulerpartlemgc  26890  bayesth  26967  erdszelem8  27231  br8  27711  supaddc  28566  supadd  28567  totbndbnd  28837  prdsbnd  28841  rrncmslem  28880  rrntotbnd  28884  isdrngo2  28913  mzpsubst  29234  rencldnfi  29309  irrapx1  29318  pellexlem3  29321  pellexlem5  29323  infmrgelbi  29368  pellqrex  29369  pellfundge  29372  rmspecfund  29399  congtr  29457  acongeq  29475  bezoutr  29477  jm2.20nn  29495  jm2.25lem1  29496  jm2.26  29500  expdiophlem1  29519  hbtlem2  29629  stoweidlem1  29945  stoweidlem20  29964  stoweidlem24  29968  stoweidlem34  29978  stoweidlem45  29989  stoweidlem60  30004  elovmpt3rab1  30312  usgra2adedgspth  30454  difelfznle  30637  2pthfrgra  30752  vdn1frgrav2  30767  vdgn1frgrav2  30768  frgrawopreg  30791  frrusgraord  30813  numclwwlk2lem1  30844  numclwwlk3  30851  frgrareg  30859  coe1fzgsumdlem  30991  lincresunit3  31148  pmatcoe1fsupp  31193  mat2pmatlin  31225  decpmatmullem  31259  pmatcollpw1lem1  31262  pmatcollpw1lem2  31263  pm2mpghm  31304  cpscmat  31329  cp0mat  31333  cpidmat  31334  cpmadugsumlemB  31361  cpmadugsumlemC  31362  cpmadugsumlemF  31363  lsatcmp  32987  lcvexchlem2  33019  lcvexchlem3  33020  ncvr1  33256  cvrletrN  33257  cvrnbtwn3  33260  cvrnrefN  33266  cvrcmp  33267  0ltat  33275  atnle0  33293  atlen0  33294  cvlcvr1  33323  cvrval3  33396  atle  33419  athgt  33439  1cvratex  33456  ps-2  33461  ps-2b  33465  llnnleat  33496  2atneat  33498  llnle  33501  atcvrlln  33503  llncmp  33505  2llnmat  33507  2at0mat0  33508  2atm  33510  ps-2c  33511  lplnle  33523  lplnnle2at  33524  llncvrlpln2  33540  llncvrlpln  33541  2lplnmN  33542  2llnmj  33543  2atmat  33544  lplncmp  33545  lplnexllnN  33547  2llnm2N  33551  2llnm4  33553  lvolnle3at  33565  4atlem3a  33580  4atlem3b  33581  4atlem10  33589  4atlem11  33592  4atlem12  33595  lplncvrlvol2  33598  lplncvrlvol  33599  lvolcmp  33600  2lplnm2N  33604  2lplnmj  33605  dalempjsen  33636  dalemcea  33643  dalem2  33644  dalemdea  33645  dalem9  33655  dalem16  33662  dalemcjden  33675  dalem21  33677  dalem23  33679  dalem39  33694  dalem54  33709  dalem60  33715  cdlemb  33777  elpadd2at  33789  paddasslem4  33806  paddasslem7  33809  paddasslem15  33817  paddasslem16  33818  pmodlem1  33829  pmodlem2  33830  llnexchb2  33852  pclfinclN  33933  osumcllem9N  33947  pmapojoinN  33951  pexmidN  33952  pl42lem1N  33962  lhp0lt  33986  lhpexle1  33991  lhpexle2lem  33992  lhpexle3lem  33994  lhprelat3N  34023  ltrnid  34118  trlval3  34170  arglem1N  34173  cdlemc5  34178  cdleme3b  34212  cdleme3c  34213  cdleme3h  34218  cdleme7e  34230  cdleme7ga  34231  cdleme20l1  34303  cdleme20l2  34304  cdleme20l  34305  cdleme22b  34324  cdlemefrs29clN  34382  cdlemefrs32fva  34383  cdlemeg46fvcl  34489  cdlemeg46c  34496  cdlemeg46fvaw  34499  cdlemeg46req  34512  cdleme48fgv  34521  cdlemf1  34544  cdlemg1cex  34571  cdlemg2dN  34573  cdlemg2ce  34575  cdlemg12e  34630  cdlemg35  34696  cdlemh  34800  tendocan  34807  cdlemk28-3  34891  tendoex  34958  dih1  35270  dihmeetlem9N  35299  dihlspsnssN  35316  dihlspsnat  35317  lcfrlem23  35549
  Copyright terms: Public domain W3C validator