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

Theorem syl31anc 1214
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 1161 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 654 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  syl32anc  1219  thema4b  1588  smo11  6811  omeulem2  7010  oeeui  7029  oaabs2  7072  omabs  7074  omxpenlem  7400  map2xp  7469  mapdom2  7470  fsuppsssupp  7624  cantnflt  7868  cantnfltOLD  7898  cnfcom  7921  cnfcomOLD  7929  mapcdaen  8341  pwsdompw  8361  cofsmo  8426  fin1a2lem4  8560  ltmul12a  10173  lt2msq1  10203  ledivp1  10222  lemul1ad  10260  lemul2ad  10261  supmul1  10283  supmul  10286  rpnnen1lem3  10969  rpnnen1lem5  10971  lediv2ad  11037  xaddge0  11209  xadddi  11246  xadddi2  11248  supicc  11420  supiccub  11421  supicclub  11422  flval3  11647  modidmul0  11718  fseqsupubi  11784  expcan  11900  ltexp2  11901  ltexp2r  11904  expubnd  11908  ltexp2rd  12016  ltexp2d  12021  leexp2d  12022  expcand  12023  swrdid  12305  swrd0fv  12319  swrds1  12329  ccatswrd  12334  swrdccat2  12336  swrdccatin2  12362  swrdccatin12lem2  12364  swrdccatin12lem3  12365  splfv1  12381  cshwidxmod  12424  o1fsum  13259  mertenslem1  13327  eftlub  13376  rpnnen2lem4  13483  ruclem12  13506  dvdsadd  13554  3dvds  13579  divalgmod  13593  bitsmod  13615  bitsinv1lem  13620  bezoutlem4  13708  gcdeq  13719  rplpwr  13723  sqgcd  13725  rpmulgcd2  13774  isprm5  13781  divgcdodd  13788  rpdvds  13793  divnumden  13809  crt  13836  phimullem  13837  modprm0  13856  modprmn0modprm0  13858  coprimeprodsq2  13860  pythagtriplem19  13883  pockthlem  13949  prmunb  13958  prmreclem3  13962  prmreclem6  13965  ramub  14057  ramz  14069  pmtrprfv  15939  pmtrprfv3  15940  mndodcong  16025  odngen  16056  pgpfi  16084  pgpssslw  16093  sylow2blem3  16101  lsmless1  16138  lsmless2  16139  lsmless12  16140  lsmmod2  16153  pj1id  16176  odadd2  16311  gexexlem  16314  ablfacrplem  16540  ablfacrp  16541  ablfac1b  16545  ablfac1eu  16548  pgpfac1lem2  16550  lsmssspx  17091  lspsncv0  17149  coe1subfv  17618  znunit  17838  uvcvvcl2  18055  uvcvv1  18056  uvcvv0  18057  mdetunilem2  18261  clsndisj  18521  neiptopnei  18578  rnelfm  19368  fmfnfmlem2  19370  fmfnfm  19373  flimss1  19388  isfcf  19449  cnextfun  19478  cnextfvval  19479  cnextf  19480  cnextcn  19481  cnextfres  19482  ustuqtop1  19658  utopsnneiplem  19664  xblss2ps  19818  xblss2  19819  stdbdxmet  19932  metcnpi3  19963  metustexhalfOLD  19980  metustexhalf  19981  nmoi  20149  nmoi2  20151  nmoco  20158  blcvx  20217  icccmplem2  20242  icccmplem3  20243  reconnlem2  20246  xrge0gsumle  20252  metds0  20268  metdstri  20269  metdseq0  20272  lebnumlem3  20377  nmoleub2lem  20511  bcthlem5  20681  minveclem2  20755  minveclem3b  20757  minveclem4  20761  minveclem6  20763  icombl  20887  cncombf  20978  mbflimsup  20986  itg2monolem1  21070  itg2mono  21073  itg2cnlem1  21081  itg2cnlem2  21082  bddmulibl  21158  ellimc2  21194  cpnord  21251  cpnres  21253  dvmulbr  21255  dvcobr  21262  dvlipcn  21308  dvlip2  21309  c1liplem1  21310  dvivthlem1  21322  lhop1lem  21327  lhop1  21328  dvfsumlem2  21341  itgsubstlem  21362  deg1add  21460  deg1sublt  21467  ply1remlem  21519  plyeq0lem  21563  taylthlem2  21724  ulmdvlem3  21752  abelthlem7  21788  pilem2  21802  pilem3  21803  pige3  21864  logccv  21993  cxpaddlelem  22074  cvxcl  22263  fsumharmonic  22290  ftalem5  22299  dvdsdivcl  22406  dvdsmulf1o  22419  bposlem1  22508  lgsqr  22570  lgsquad2lem2  22583  2sqlem8a  22595  2sqlem8  22596  dchrmusum2  22628  dchrvmasumiflem1  22635  dchrisum0flblem1  22642  dchrisum0lem1b  22649  pntlem3  22743  axsegcon  22996  ax5seglem1  22997  ax5seglem2  22998  axlowdimlem6  23016  axeuclidlem  23031  axcontlem7  23039  axcontlem9  23041  axcontlem10  23042  cusgrasize2inds  23208  vdgrun  23394  vdgrfiun  23395  vdgr1d  23396  vdgr1b  23397  vdgr1a  23399  nmoub3i  23996  ubthlem3  24096  minvecolem2  24099  minvecolem4  24104  minvecolem5  24105  minvecolem6  24106  htthlem  24142  pjpjpre  24645  chscllem1  24863  chscllem2  24864  chscllem3  24865  cnlnadjlem2  25295  leopnmid  25365  br8d  25766  ogrpaddlt  26005  archirngz  26030  ornglmullt  26128  orngrmullt  26129  elrhmunit  26141  kerf1hrm  26145  qqhval2lem  26264  qqhnm  26273  qqhucn  26275  esumcst  26368  esumpcvgval  26381  measunl  26484  dya2iocbrsiga  26544  dya2icobrsiga  26545  sibfof  26574  oddpwdc  26585  eulerpartlemgc  26593  bayesth  26670  erdszelem8  26934  br8  27413  supaddc  28261  supadd  28262  totbndbnd  28532  prdsbnd  28536  rrncmslem  28575  rrntotbnd  28579  isdrngo2  28608  mzpsubst  28930  rencldnfi  29005  irrapx1  29014  pellexlem3  29017  pellexlem5  29019  infmrgelbi  29064  pellqrex  29065  pellfundge  29068  rmspecfund  29095  congtr  29153  acongeq  29171  bezoutr  29173  jm2.20nn  29191  jm2.25lem1  29192  jm2.26  29196  expdiophlem1  29215  hbtlem2  29325  stoweidlem1  29642  stoweidlem24  29665  stoweidlem34  29675  stoweidlem45  29686  stoweidlem60  29701  elovmpt3rab1  30009  usgra2adedgspth  30151  difelfznle  30334  2pthfrgra  30449  vdn1frgrav2  30464  vdgn1frgrav2  30465  frgrawopreg  30488  frrusgraord  30510  numclwwlk2lem1  30541  numclwwlk3  30548  frgrareg  30556  lincresunit3  30724  lsatcmp  32221  lcvexchlem2  32253  lcvexchlem3  32254  ncvr1  32490  cvrletrN  32491  cvrnbtwn3  32494  cvrnrefN  32500  cvrcmp  32501  0ltat  32509  atnle0  32527  atlen0  32528  cvlcvr1  32557  cvrval3  32630  atle  32653  athgt  32673  1cvratex  32690  ps-2  32695  ps-2b  32699  llnnleat  32730  2atneat  32732  llnle  32735  atcvrlln  32737  llncmp  32739  2llnmat  32741  2at0mat0  32742  2atm  32744  ps-2c  32745  lplnle  32757  lplnnle2at  32758  llncvrlpln2  32774  llncvrlpln  32775  2lplnmN  32776  2llnmj  32777  2atmat  32778  lplncmp  32779  lplnexllnN  32781  2llnm2N  32785  2llnm4  32787  lvolnle3at  32799  4atlem3a  32814  4atlem3b  32815  4atlem10  32823  4atlem11  32826  4atlem12  32829  lplncvrlvol2  32832  lplncvrlvol  32833  lvolcmp  32834  2lplnm2N  32838  2lplnmj  32839  dalempjsen  32870  dalemcea  32877  dalem2  32878  dalemdea  32879  dalem9  32889  dalem16  32896  dalemcjden  32909  dalem21  32911  dalem23  32913  dalem39  32928  dalem54  32943  dalem60  32949  cdlemb  33011  elpadd2at  33023  paddasslem4  33040  paddasslem7  33043  paddasslem15  33051  paddasslem16  33052  pmodlem1  33063  pmodlem2  33064  llnexchb2  33086  pclfinclN  33167  osumcllem9N  33181  pmapojoinN  33185  pexmidN  33186  pl42lem1N  33196  lhp0lt  33220  lhpexle1  33225  lhpexle2lem  33226  lhpexle3lem  33228  lhprelat3N  33257  ltrnid  33352  trlval3  33404  arglem1N  33407  cdlemc5  33412  cdleme3b  33446  cdleme3c  33447  cdleme3h  33452  cdleme7e  33464  cdleme7ga  33465  cdleme20l1  33537  cdleme20l2  33538  cdleme20l  33539  cdleme22b  33558  cdlemefrs29clN  33616  cdlemefrs32fva  33617  cdlemeg46fvcl  33723  cdlemeg46c  33730  cdlemeg46fvaw  33733  cdlemeg46req  33746  cdleme48fgv  33755  cdlemf1  33778  cdlemg1cex  33805  cdlemg2dN  33807  cdlemg2ce  33809  cdlemg12e  33864  cdlemg35  33930  cdlemh  34034  tendocan  34041  cdlemk28-3  34125  tendoex  34192  dih1  34504  dihmeetlem9N  34533  dihlspsnssN  34550  dihlspsnat  34551  lcfrlem23  34783
  Copyright terms: Public domain W3C validator