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

Theorem syl31anc 1185
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 1132 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 642 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  syl32anc  1190  smo11  6381  omeulem2  6581  oeeui  6600  oaabs2  6643  omabs  6645  omxpenlem  6963  map2xp  7031  mapdom2  7032  cantnflt  7373  cnfcom  7403  mapcdaen  7810  pwsdompw  7830  cofsmo  7895  fin1a2lem4  8029  ltmul12a  9612  lt2msq1  9639  ledivp1  9658  lemul1ad  9696  lemul2ad  9697  supmul1  9719  supmul  9722  rpnnen1lem3  10344  rpnnen1lem5  10346  lediv2ad  10412  xaddge0  10578  xadddi  10615  xadddi2  10617  flval3  10945  fseqsupubi  11040  expcan  11154  ltexp2  11155  ltexp2r  11158  expubnd  11162  ltexp2rd  11269  ltexp2d  11274  leexp2d  11275  expcand  11276  swrdid  11458  ccatswrd  11459  swrdccat2  11461  splfv1  11470  swrds1  11473  o1fsum  12271  mertenslem1  12340  eftlub  12389  rpnnen2lem4  12496  ruclem12  12519  dvdsadd  12567  3dvds  12591  divalgmod  12605  bitsmod  12627  bitsinv1lem  12632  bezoutlem4  12720  gcdeq  12731  rplpwr  12735  sqgcd  12737  rpmulgcd2  12784  isprm5  12791  divgcdodd  12798  rpdvds  12803  divnumden  12819  crt  12846  phimullem  12847  coprimeprodsq2  12863  pythagtriplem19  12886  pockthlem  12952  prmunb  12961  prmreclem3  12965  prmreclem6  12968  ramub  13060  ramz  13072  mndodcong  14857  odngen  14888  pgpfi  14916  pgpssslw  14925  sylow2blem3  14933  lsmless1  14970  lsmless2  14971  lsmless12  14972  lsmmod2  14985  pj1id  15008  odadd2  15141  gexexlem  15144  ablfacrplem  15300  ablfacrp  15301  ablfac1b  15305  ablfac1eu  15308  pgpfac1lem2  15310  lsmssspx  15841  lspsncv0  15899  coe1subfv  16343  znunit  16517  clsndisj  16812  rnelfm  17648  fmfnfmlem2  17650  fmfnfm  17653  flimss1  17668  isfcf  17729  xblss2  17958  stdbdxmet  18061  metcnpi3  18092  nmoi  18237  nmoi2  18239  nmoco  18246  blcvx  18304  icccmplem2  18328  icccmplem3  18329  reconnlem2  18332  xrge0gsumle  18338  metds0  18354  metdstri  18355  metdseq0  18358  lebnumlem3  18461  nmoleub2lem  18595  bcthlem5  18750  minveclem2  18790  minveclem3b  18792  minveclem4  18796  minveclem6  18798  icombl  18921  cncombf  19013  mbflimsup  19021  itg2monolem1  19105  itg2mono  19108  itg2cnlem1  19116  itg2cnlem2  19117  bddmulibl  19193  ellimc2  19227  cpnord  19284  cpnres  19286  dvmulbr  19288  dvcobr  19295  dvlipcn  19341  dvlip2  19342  c1liplem1  19343  dvivthlem1  19355  lhop1lem  19360  lhop1  19361  dvfsumlem2  19374  itgsubstlem  19395  deg1add  19489  deg1sublt  19496  ply1remlem  19548  plyeq0lem  19592  taylthlem2  19753  ulmdvlem3  19779  abelthlem7  19814  pilem2  19828  pilem3  19829  pige3  19885  logccv  20010  cxpaddlelem  20091  cvxcl  20279  fsumharmonic  20305  ftalem5  20314  dvdsdivcl  20421  dvdsmulf1o  20434  bposlem1  20523  lgsqr  20585  lgsquad2lem2  20598  2sqlem8a  20610  2sqlem8  20611  dchrmusum2  20643  dchrvmasumiflem1  20650  dchrisum0flblem1  20657  dchrisum0lem1b  20664  pntlem3  20758  nmoub3i  21351  ubthlem3  21451  minvecolem2  21454  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  htthlem  21497  pjpjpre  21998  chscllem1  22216  chscllem2  22217  chscllem3  22218  cnlnadjlem2  22648  leopnmid  22718  ballotlemsgt1  23069  ballotlemsel1i  23071  snunioc  23267  esumcst  23436  esumpcvgval  23446  dya2iocbrsiga  23578  bayesth  23642  erdszelem8  23729  vdgrun  23893  vdgr1d  23894  vdgr1b  23895  vdgr1a  23897  br8  24113  axsegcon  24555  ax5seglem1  24556  ax5seglem2  24557  axlowdimlem6  24575  axeuclidlem  24590  axcontlem7  24598  axcontlem9  24600  axcontlem10  24601  areacirclem3  24926  cmptdst  25568  cmptdst2  25571  limnumrr  25622  flfneic  25624  flfneicn  25625  idcatfun  25941  rocatval  25959  indcls2  25996  totbndbnd  26513  prdsbnd  26517  rrncmslem  26556  rrntotbnd  26560  isdrngo2  26589  mzpsubst  26826  rencldnfi  26904  irrapx1  26913  pellexlem3  26916  pellexlem5  26918  infmrgelbi  26963  pellqrex  26964  pellfundge  26967  rmspecfund  26994  congtr  27052  acongeq  27070  bezoutr  27072  jm2.20nn  27090  jm2.25lem1  27091  jm2.26  27095  expdiophlem1  27114  uvcvvcl2  27237  uvcvv1  27238  uvcvv0  27239  hbtlem2  27328  pmtrprfv  27396  lsatcmp  29193  lcvexchlem2  29225  lcvexchlem3  29226  ncvr1  29462  cvrletrN  29463  cvrnbtwn3  29466  cvrnrefN  29472  cvrcmp  29473  0ltat  29481  atnle0  29499  atlen0  29500  cvlcvr1  29529  cvrval3  29602  atle  29625  athgt  29645  1cvratex  29662  ps-2  29667  ps-2b  29671  llnnleat  29702  2atneat  29704  llnle  29707  atcvrlln  29709  llncmp  29711  2llnmat  29713  2at0mat0  29714  2atm  29716  ps-2c  29717  lplnle  29729  lplnnle2at  29730  llncvrlpln2  29746  llncvrlpln  29747  2lplnmN  29748  2llnmj  29749  2atmat  29750  lplncmp  29751  lplnexllnN  29753  2llnm2N  29757  2llnm4  29759  lvolnle3at  29771  4atlem3a  29786  4atlem3b  29787  4atlem10  29795  4atlem11  29798  4atlem12  29801  lplncvrlvol2  29804  lplncvrlvol  29805  lvolcmp  29806  2lplnm2N  29810  2lplnmj  29811  dalempjsen  29842  dalemcea  29849  dalem2  29850  dalemdea  29851  dalem9  29861  dalem16  29868  dalemcjden  29881  dalem21  29883  dalem23  29885  dalem39  29900  dalem54  29915  dalem60  29921  cdlemb  29983  elpadd2at  29995  paddasslem4  30012  paddasslem7  30015  paddasslem15  30023  paddasslem16  30024  pmodlem1  30035  pmodlem2  30036  llnexchb2  30058  pclfinclN  30139  osumcllem9N  30153  pmapojoinN  30157  pexmidN  30158  pl42lem1N  30168  lhp0lt  30192  lhpexle1  30197  lhpexle2lem  30198  lhpexle3lem  30200  lhprelat3N  30229  ltrnid  30324  trlval3  30376  arglem1N  30379  cdlemc5  30384  cdleme3b  30418  cdleme3c  30419  cdleme3h  30424  cdleme7e  30436  cdleme7ga  30437  cdleme20l1  30509  cdleme20l2  30510  cdleme20l  30511  cdleme22b  30530  cdlemefrs29clN  30588  cdlemefrs32fva  30589  cdlemeg46fvcl  30695  cdlemeg46c  30702  cdlemeg46fvaw  30705  cdlemeg46req  30718  cdleme48fgv  30727  cdlemf1  30750  cdlemg1cex  30777  cdlemg2dN  30779  cdlemg2ce  30781  cdlemg12e  30836  cdlemg35  30902  cdlemh  31006  tendocan  31013  cdlemk28-3  31097  tendoex  31164  dih1  31476  dihmeetlem9N  31505  dihlspsnssN  31522  dihlspsnat  31523  lcfrlem23  31755
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator