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

Theorem syl31anc 1187
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 1134 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 643 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  syl32anc  1192  smo11  6618  omeulem2  6818  oeeui  6837  oaabs2  6880  omabs  6882  omxpenlem  7201  map2xp  7269  mapdom2  7270  cantnflt  7619  cnfcom  7649  mapcdaen  8056  pwsdompw  8076  cofsmo  8141  fin1a2lem4  8275  ltmul12a  9858  lt2msq1  9885  ledivp1  9904  lemul1ad  9942  lemul2ad  9943  supmul1  9965  supmul  9968  rpnnen1lem3  10594  rpnnen1lem5  10596  lediv2ad  10662  xaddge0  10829  xadddi  10866  xadddi2  10868  flval3  11214  fseqsupubi  11309  expcan  11424  ltexp2  11425  ltexp2r  11428  expubnd  11432  ltexp2rd  11539  ltexp2d  11544  leexp2d  11545  expcand  11546  swrdid  11764  ccatswrd  11765  swrdccat2  11767  splfv1  11776  swrds1  11779  o1fsum  12584  mertenslem1  12653  eftlub  12702  rpnnen2lem4  12809  ruclem12  12832  dvdsadd  12880  3dvds  12904  divalgmod  12918  bitsmod  12940  bitsinv1lem  12945  bezoutlem4  13033  gcdeq  13044  rplpwr  13048  sqgcd  13050  rpmulgcd2  13097  isprm5  13104  divgcdodd  13111  rpdvds  13116  divnumden  13132  crt  13159  phimullem  13160  coprimeprodsq2  13176  pythagtriplem19  13199  pockthlem  13265  prmunb  13274  prmreclem3  13278  prmreclem6  13281  ramub  13373  ramz  13385  mndodcong  15172  odngen  15203  pgpfi  15231  pgpssslw  15240  sylow2blem3  15248  lsmless1  15285  lsmless2  15286  lsmless12  15287  lsmmod2  15300  pj1id  15323  odadd2  15456  gexexlem  15459  ablfacrplem  15615  ablfacrp  15616  ablfac1b  15620  ablfac1eu  15623  pgpfac1lem2  15625  lsmssspx  16152  lspsncv0  16210  coe1subfv  16651  znunit  16836  clsndisj  17131  neiptopnei  17188  rnelfm  17977  fmfnfmlem2  17979  fmfnfm  17982  flimss1  17997  isfcf  18058  cnextfun  18087  cnextfvval  18088  cnextf  18089  cnextcn  18090  cnextfres  18091  ustuqtop1  18263  utopsnneiplem  18269  xblss2ps  18423  xblss2  18424  stdbdxmet  18537  metcnpi3  18568  metustexhalfOLD  18585  metustexhalf  18586  nmoi  18754  nmoi2  18756  nmoco  18763  blcvx  18821  icccmplem2  18846  icccmplem3  18847  reconnlem2  18850  xrge0gsumle  18856  metds0  18872  metdstri  18873  metdseq0  18876  lebnumlem3  18980  nmoleub2lem  19114  bcthlem5  19273  minveclem2  19319  minveclem3b  19321  minveclem4  19325  minveclem6  19327  icombl  19450  cncombf  19542  mbflimsup  19550  itg2monolem1  19634  itg2mono  19637  itg2cnlem1  19645  itg2cnlem2  19646  bddmulibl  19722  ellimc2  19756  cpnord  19813  cpnres  19815  dvmulbr  19817  dvcobr  19824  dvlipcn  19870  dvlip2  19871  c1liplem1  19872  dvivthlem1  19884  lhop1lem  19889  lhop1  19890  dvfsumlem2  19903  itgsubstlem  19924  deg1add  20018  deg1sublt  20025  ply1remlem  20077  plyeq0lem  20121  taylthlem2  20282  ulmdvlem3  20310  abelthlem7  20346  pilem2  20360  pilem3  20361  pige3  20417  logccv  20546  cxpaddlelem  20627  cvxcl  20815  fsumharmonic  20842  ftalem5  20851  dvdsdivcl  20958  dvdsmulf1o  20971  bposlem1  21060  lgsqr  21122  lgsquad2lem2  21135  2sqlem8a  21147  2sqlem8  21148  dchrmusum2  21180  dchrvmasumiflem1  21187  dchrisum0flblem1  21194  dchrisum0lem1b  21201  pntlem3  21295  cusgrasize2inds  21478  vdgrun  21664  vdgrfiun  21665  vdgr1d  21666  vdgr1b  21667  vdgr1a  21669  nmoub3i  22266  ubthlem3  22366  minvecolem2  22369  minvecolem4  22374  minvecolem5  22375  minvecolem6  22376  htthlem  22412  pjpjpre  22913  chscllem1  23131  chscllem2  23132  chscllem3  23133  cnlnadjlem2  23563  leopnmid  23633  ofldaddlt  24233  elrhmunit  24250  kerf1hrm  24254  qqhval2lem  24357  qqhnm  24366  qqhucn  24368  esumcst  24447  esumpcvgval  24460  measunl  24562  dya2iocbrsiga  24617  dya2icobrsiga  24618  bayesth  24689  erdszelem8  24876  br8  25371  axsegcon  25858  ax5seglem1  25859  ax5seglem2  25860  axlowdimlem6  25878  axeuclidlem  25893  axcontlem7  25901  axcontlem9  25903  axcontlem10  25904  supaddc  26228  supadd  26229  areacirclem3  26283  totbndbnd  26489  prdsbnd  26493  rrncmslem  26532  rrntotbnd  26536  isdrngo2  26565  mzpsubst  26796  rencldnfi  26873  irrapx1  26882  pellexlem3  26885  pellexlem5  26887  infmrgelbi  26932  pellqrex  26933  pellfundge  26936  rmspecfund  26963  congtr  27021  acongeq  27039  bezoutr  27041  jm2.20nn  27059  jm2.25lem1  27060  jm2.26  27064  expdiophlem1  27083  uvcvvcl2  27205  uvcvv1  27206  uvcvv0  27207  hbtlem2  27296  pmtrprfv  27364  stoweidlem1  27717  stoweidlem24  27740  stoweidlem34  27750  stoweidlem45  27761  stoweidlem60  27776  modidmul0  28138  swrdccatin2  28176  swrdccatin12lem3  28178  swrdccatin12lem4  28179  modprm0  28194  usgra2adedgspth  28268  2pthfrgra  28338  vdn1frgrav2  28353  vdgn1frgrav2  28354  frgrawopreg  28375  lsatcmp  29738  lcvexchlem2  29770  lcvexchlem3  29771  ncvr1  30007  cvrletrN  30008  cvrnbtwn3  30011  cvrnrefN  30017  cvrcmp  30018  0ltat  30026  atnle0  30044  atlen0  30045  cvlcvr1  30074  cvrval3  30147  atle  30170  athgt  30190  1cvratex  30207  ps-2  30212  ps-2b  30216  llnnleat  30247  2atneat  30249  llnle  30252  atcvrlln  30254  llncmp  30256  2llnmat  30258  2at0mat0  30259  2atm  30261  ps-2c  30262  lplnle  30274  lplnnle2at  30275  llncvrlpln2  30291  llncvrlpln  30292  2lplnmN  30293  2llnmj  30294  2atmat  30295  lplncmp  30296  lplnexllnN  30298  2llnm2N  30302  2llnm4  30304  lvolnle3at  30316  4atlem3a  30331  4atlem3b  30332  4atlem10  30340  4atlem11  30343  4atlem12  30346  lplncvrlvol2  30349  lplncvrlvol  30350  lvolcmp  30351  2lplnm2N  30355  2lplnmj  30356  dalempjsen  30387  dalemcea  30394  dalem2  30395  dalemdea  30396  dalem9  30406  dalem16  30413  dalemcjden  30426  dalem21  30428  dalem23  30430  dalem39  30445  dalem54  30460  dalem60  30466  cdlemb  30528  elpadd2at  30540  paddasslem4  30557  paddasslem7  30560  paddasslem15  30568  paddasslem16  30569  pmodlem1  30580  pmodlem2  30581  llnexchb2  30603  pclfinclN  30684  osumcllem9N  30698  pmapojoinN  30702  pexmidN  30703  pl42lem1N  30713  lhp0lt  30737  lhpexle1  30742  lhpexle2lem  30743  lhpexle3lem  30745  lhprelat3N  30774  ltrnid  30869  trlval3  30921  arglem1N  30924  cdlemc5  30929  cdleme3b  30963  cdleme3c  30964  cdleme3h  30969  cdleme7e  30981  cdleme7ga  30982  cdleme20l1  31054  cdleme20l2  31055  cdleme20l  31056  cdleme22b  31075  cdlemefrs29clN  31133  cdlemefrs32fva  31134  cdlemeg46fvcl  31240  cdlemeg46c  31247  cdlemeg46fvaw  31250  cdlemeg46req  31263  cdleme48fgv  31272  cdlemf1  31295  cdlemg1cex  31322  cdlemg2dN  31324  cdlemg2ce  31326  cdlemg12e  31381  cdlemg35  31447  cdlemh  31551  tendocan  31558  cdlemk28-3  31642  tendoex  31709  dih1  32021  dihmeetlem9N  32050  dihlspsnssN  32067  dihlspsnat  32068  lcfrlem23  32300
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator