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

Theorem syl31anc 1229
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 1174 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 659 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  syl32anc  1234  stoic4b  1616  elovmpt3rab1  6509  smo11  7027  omeulem2  7224  oeeui  7243  oaabs2  7286  omabs  7288  omxpenlem  7611  map2xp  7680  mapdom2  7681  fsuppsssupp  7837  cantnflt  8082  cantnfltOLD  8112  cnfcom  8135  cnfcomOLD  8143  mapcdaen  8555  pwsdompw  8575  cofsmo  8640  fin1a2lem4  8774  ltmul12a  10394  lt2msq1  10423  ledivp1  10442  lemul1ad  10480  lemul2ad  10481  supmul1  10503  supmul  10506  rpnnen1lem3  11211  rpnnen1lem5  11213  lediv2ad  11281  xaddge0  11453  xadddi  11490  xadddi2  11492  supicc  11671  supiccub  11672  supicclub  11673  difelfznle  11793  flval3  11932  modidmul0OLD  12005  fseqsupubi  12073  expcan  12203  ltexp2  12204  ltexp2r  12207  expubnd  12211  ltexp2rd  12319  ltexp2d  12324  leexp2d  12325  expcand  12326  swrdid  12647  swrd0fv  12658  swrds1  12670  ccatswrd  12675  swrdccat2  12677  swrdccatin2  12706  swrdccatin12lem2  12708  swrdccatin12lem3  12709  splfv1  12725  cshwidxmod  12768  o1fsum  13712  mertenslem1  13778  eftlub  13929  rpnnen2lem4  14038  ruclem12  14061  dvdsadd  14111  3dvds  14137  divalgmod  14151  bitsmod  14173  bitsinv1lem  14178  bezoutlem4  14266  gcdeq  14277  rplpwr  14281  sqgcd  14283  rpmulgcd2  14333  isprm5  14340  divgcdodd  14347  rpdvds  14352  divnumden  14368  crt  14395  phimullem  14396  modprm0  14417  modprmn0modprm0  14419  coprimeprodsq2  14421  pythagtriplem19  14444  pockthlem  14510  prmunb  14519  prmreclem3  14523  prmreclem6  14526  ramub  14618  ramz  14630  pmtrprfv  16680  pmtrprfv3  16681  mndodcong  16768  odngen  16799  pgpfi  16827  pgpssslw  16836  sylow2blem3  16844  lsmless1  16881  lsmless2  16882  lsmless12  16883  lsmmod2  16896  pj1id  16919  odadd2  17057  gexexlem  17060  ablfacrplem  17314  ablfacrp  17315  ablfac1b  17319  ablfac1eu  17322  pgpfac1lem2  17324  kerf1hrm  17590  lsmssspx  17932  lspsncv0  17990  coe1subfv  18505  coe1fzgsumdlem  18541  znunit  18778  uvcvvcl2  18993  uvcvv1  18994  uvcvv0  18995  scmate  19182  mdetunilem2  19285  pmatcoe1fsupp  19372  mat2pmatlin  19406  decpmatmullem  19442  pmatcollpw1lem1  19445  pmatcollpw1lem2  19446  pm2mpghm  19487  chpscmat  19513  chp0mat  19517  chpidmat  19518  cpmadugsumlemB  19545  cpmadugsumlemC  19546  cpmadugsumlemF  19547  clsndisj  19746  neiptopnei  19803  rnelfm  20623  fmfnfmlem2  20625  fmfnfm  20628  flimss1  20643  isfcf  20704  cnextfun  20733  cnextfvval  20734  cnextf  20735  cnextcn  20736  cnextfres  20737  ustuqtop1  20913  utopsnneiplem  20919  xblss2ps  21073  xblss2  21074  stdbdxmet  21187  metcnpi3  21218  metustexhalfOLD  21235  metustexhalf  21236  nmoi  21404  nmoi2  21406  nmoco  21413  blcvx  21472  icccmplem2  21497  icccmplem3  21498  reconnlem2  21501  xrge0gsumle  21507  metds0  21523  metdstri  21524  metdseq0  21527  lebnumlem3  21632  nmoleub2lem  21766  bcthlem5  21936  minveclem2  22010  minveclem3b  22012  minveclem4  22016  minveclem6  22018  icombl  22143  cncombf  22234  mbflimsup  22242  itg2monolem1  22326  itg2mono  22329  itg2cnlem1  22337  itg2cnlem2  22338  bddmulibl  22414  ellimc2  22450  cpnord  22507  cpnres  22509  dvmulbr  22511  dvcobr  22518  dvlipcn  22564  dvlip2  22565  c1liplem1  22566  dvivthlem1  22578  lhop1lem  22583  lhop1  22584  dvfsumlem2  22597  itgsubstlem  22618  deg1add  22673  deg1sublt  22680  ply1remlem  22732  plyeq0lem  22776  taylthlem2  22938  ulmdvlem3  22966  abelthlem7  23002  pilem2  23016  pilem3  23017  pige3  23079  logccv  23215  cxpaddlelem  23296  cvxcl  23515  fsumharmonic  23542  ftalem5  23551  dvdsdivcl  23658  dvdsmulf1o  23671  bposlem1  23760  lgsqr  23822  lgsquad2lem2  23835  2sqlem8a  23847  2sqlem8  23848  dchrmusum2  23880  dchrvmasumiflem1  23887  dchrisum0flblem1  23894  dchrisum0lem1b  23901  pntlem3  23995  tgdim01  24102  axsegcon  24435  ax5seglem1  24436  ax5seglem2  24437  axlowdimlem6  24455  axeuclidlem  24470  axcontlem7  24478  axcontlem9  24480  axcontlem10  24481  cusgrasize2inds  24682  usgra2adedgspth  24818  vdgrun  25106  vdgrfiun  25107  vdgr1d  25108  vdgr1b  25109  vdgr1a  25111  2pthfrgra  25216  vdn1frgrav2  25230  vdgn1frgrav2  25231  frgrawopreg  25254  frrusgraord  25276  numclwwlk2lem1  25307  numclwwlk3  25314  frgrareg  25322  nmoub3i  25889  ubthlem3  25989  minvecolem2  25992  minvecolem4  25997  minvecolem5  25998  minvecolem6  25999  htthlem  26035  pjpjpre  26538  chscllem1  26756  chscllem2  26757  chscllem3  26758  cnlnadjlem2  27188  leopnmid  27258  br8d  27681  ogrpaddlt  27945  archirngz  27970  ornglmullt  28035  orngrmullt  28036  elrhmunit  28048  qqhval2lem  28199  qqhnm  28208  qqhucn  28210  esumcst  28295  esumpcvgval  28310  measunl  28427  dya2iocbrsiga  28486  dya2icobrsiga  28487  omssubadd  28511  inelcarsg  28522  carsgclctunlem2  28530  sibfof  28549  oddpwdc  28560  eulerpartlemgc  28568  bayesth  28645  erdszelem8  28909  br8  29429  supaddc  30284  supadd  30285  totbndbnd  30528  prdsbnd  30532  rrncmslem  30571  rrntotbnd  30575  isdrngo2  30604  mzpsubst  30923  rencldnfi  30997  irrapx1  31006  pellexlem3  31009  pellexlem5  31011  infmrgelbi  31056  pellqrex  31057  pellfundge  31060  rmspecfund  31087  congtr  31145  acongeq  31163  bezoutr  31165  jm2.20nn  31181  jm2.25lem1  31182  jm2.26  31186  expdiophlem1  31205  hbtlem2  31317  suprnmpt  31694  upbdrech  31747  ssfiunibd  31751  iccintsng  31805  limcrecl  31877  dvmulcncf  31964  dvdivcncf  31966  dvbdfbdioolem1  31967  ioodvbdlimc1lem2  31971  ioodvbdlimc2lem  31973  stoweidlem1  32025  stoweidlem20  32044  stoweidlem24  32048  stoweidlem34  32058  stoweidlem45  32069  stoweidlem60  32084  fourierdlem20  32151  fourierdlem31  32162  fourierdlem38  32169  fourierdlem64  32195  fourierdlem79  32210  fourierdlem94  32225  fourierdlem113  32244  fouriersw  32256  fouriercn  32257  gcdzeq  32578  pfxfv  32646  lincresunit3  33355  elbigolo1  33451  lsatcmp  35144  lcvexchlem2  35176  lcvexchlem3  35177  ncvr1  35413  cvrletrN  35414  cvrnbtwn3  35417  cvrnrefN  35423  cvrcmp  35424  0ltat  35432  atnle0  35450  atlen0  35451  cvlcvr1  35480  cvrval3  35553  atle  35576  athgt  35596  1cvratex  35613  ps-2  35618  ps-2b  35622  llnnleat  35653  2atneat  35655  llnle  35658  atcvrlln  35660  llncmp  35662  2llnmat  35664  2at0mat0  35665  2atm  35667  ps-2c  35668  lplnle  35680  lplnnle2at  35681  llncvrlpln2  35697  llncvrlpln  35698  2lplnmN  35699  2llnmj  35700  2atmat  35701  lplncmp  35702  lplnexllnN  35704  2llnm2N  35708  2llnm4  35710  lvolnle3at  35722  4atlem3a  35737  4atlem3b  35738  4atlem10  35746  4atlem11  35749  4atlem12  35752  lplncvrlvol2  35755  lplncvrlvol  35756  lvolcmp  35757  2lplnm2N  35761  2lplnmj  35762  dalempjsen  35793  dalemcea  35800  dalem2  35801  dalemdea  35802  dalem9  35812  dalem16  35819  dalemcjden  35832  dalem21  35834  dalem23  35836  dalem39  35851  dalem54  35866  dalem60  35872  cdlemb  35934  elpadd2at  35946  paddasslem4  35963  paddasslem7  35966  paddasslem15  35974  paddasslem16  35975  pmodlem1  35986  pmodlem2  35987  llnexchb2  36009  pclfinclN  36090  osumcllem9N  36104  pmapojoinN  36108  pexmidN  36109  pl42lem1N  36119  lhp0lt  36143  lhpexle1  36148  lhpexle2lem  36149  lhpexle3lem  36151  lhprelat3N  36180  ltrnid  36275  trlval3  36328  arglem1N  36331  cdlemc5  36336  cdleme3b  36370  cdleme3c  36371  cdleme3h  36376  cdleme7e  36388  cdleme7ga  36389  cdleme20l1  36462  cdleme20l2  36463  cdleme20l  36464  cdleme22b  36483  cdlemefrs29clN  36541  cdlemefrs32fva  36542  cdlemeg46fvcl  36648  cdlemeg46c  36655  cdlemeg46fvaw  36658  cdlemeg46req  36671  cdleme48fgv  36680  cdlemf1  36703  cdlemg1cex  36730  cdlemg2dN  36732  cdlemg2ce  36734  cdlemg12e  36789  cdlemg35  36855  cdlemh  36959  tendocan  36966  cdlemk28-3  37050  tendoex  37117  dih1  37429  dihmeetlem9N  37458  dihlspsnssN  37475  dihlspsnat  37476  lcfrlem23  37708  suprubd  38507  suprleubrd  38514  suprlubrd  38518
  Copyright terms: Public domain W3C validator