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

Theorem syl31anc 1267
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 1185 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 665 1  |-  ( ph  ->  et )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  syl32anc  1272  stoic4b  1658  elovmpt3rab1  6541  smo11  7091  omeulem2  7292  oeeui  7311  oaabs2  7354  omabs  7356  omxpenlem  7679  map2xp  7748  mapdom2  7749  fsuppsssupp  7905  cantnflt  8176  cnfcom  8204  mapcdaen  8612  pwsdompw  8632  cofsmo  8697  fin1a2lem4  8831  ltmul12a  10460  lt2msq1  10489  ledivp1  10508  lemul1ad  10546  lemul2ad  10547  supaddc  10574  supadd  10575  supmul1  10576  supmul  10579  rpnnen1lem3  11292  rpnnen1lem5  11294  lediv2ad  11363  xaddge0  11544  xadddi  11581  xadddi2  11583  supicc  11778  supiccub  11779  supicclub  11780  difelfznle  11903  flval3  12047  modidmul0OLD  12120  fseqsupubi  12188  expcan  12322  ltexp2  12323  ltexp2r  12326  expubnd  12330  ltexp2rd  12437  ltexp2d  12442  leexp2d  12443  expcand  12444  swrdid  12769  swrd0fv  12780  swrds1  12792  ccatswrd  12797  swrdccat2  12799  swrdccatin2  12828  swrdccatin12lem2  12830  swrdccatin12lem3  12831  splfv1  12847  cshwidxmod  12890  o1fsum  13851  mertenslem1  13918  eftlub  14141  rpnnen2lem4  14248  ruclem12  14271  dvdsadd  14321  3dvds  14347  divalgmod  14362  bitsmod  14384  bitsinv1lem  14389  bezoutlem4  14480  gcdeq  14491  rplpwr  14495  sqgcd  14497  isprm5  14622  divgcdodd  14624  rpmulgcd2  14633  rpdvds  14647  coprmproddvdslem  14650  divnumden  14668  crt  14695  phimullem  14696  modprm0  14719  modprmn0modprm0  14721  coprimeprodsq2  14723  pythagtriplem19  14746  pockthlem  14812  prmunb  14821  prmreclem3  14825  prmreclem6  14828  ramub  14933  ramz  14946  pmtrprfv  17045  pmtrprfv3  17046  mndodcong  17133  odngen  17164  pgpfi  17192  pgpssslw  17201  sylow2blem3  17209  lsmless1  17246  lsmless2  17247  lsmless12  17248  lsmmod2  17261  pj1id  17284  odadd2  17422  gexexlem  17425  ablfacrplem  17633  ablfacrp  17634  ablfac1b  17638  ablfac1eu  17641  pgpfac1lem2  17643  kerf1hrm  17906  lsmssspx  18246  lspsncv0  18304  coe1subfv  18794  coe1fzgsumdlem  18830  znunit  19065  uvcvvcl2  19277  uvcvv1  19278  uvcvv0  19279  scmate  19466  mdetunilem2  19569  pmatcoe1fsupp  19656  mat2pmatlin  19690  decpmatmullem  19726  pmatcollpw1lem1  19729  pmatcollpw1lem2  19730  pm2mpghm  19771  chpscmat  19797  chp0mat  19801  chpidmat  19802  cpmadugsumlemB  19829  cpmadugsumlemC  19830  cpmadugsumlemF  19831  clsndisj  20022  neiptopnei  20079  rnelfm  20899  fmfnfmlem2  20901  fmfnfm  20904  flimss1  20919  isfcf  20980  cnextfun  21010  cnextfvval  21011  cnextf  21012  cnextcn  21013  cnextfres1  21014  ustuqtop1  21187  utopsnneiplem  21193  xblss2ps  21347  xblss2  21348  stdbdxmet  21461  metcnpi3  21492  metustexhalf  21502  nmoi  21660  nmoi2  21662  nmoco  21669  blcvx  21727  icccmplem2  21752  icccmplem3  21753  reconnlem2  21756  xrge0gsumle  21762  metds0  21778  metdstri  21779  metdseq0  21782  lebnumlem3  21887  nmoleub2lem  22021  bcthlem5  22189  minveclem2  22261  minveclem3b  22263  minveclem4  22267  minveclem6  22269  icombl  22394  cncombf  22491  mbflimsup  22500  mbflimsupOLD  22501  itg2monolem1  22585  itg2mono  22588  itg2cnlem1  22596  itg2cnlem2  22597  bddmulibl  22673  ellimc2  22709  cpnord  22766  cpnres  22768  dvmulbr  22770  dvcobr  22777  dvlipcn  22823  dvlip2  22824  c1liplem1  22825  dvivthlem1  22837  lhop1lem  22842  lhop1  22843  dvfsumlem2  22856  itgsubstlem  22877  deg1add  22929  deg1sublt  22936  ply1remlem  22988  plyeq0lem  23032  taylthlem2  23194  ulmdvlem3  23222  abelthlem7  23258  pilem2  23272  pilem2OLD  23273  pilem3  23274  pilem3OLD  23275  pige3  23337  logccv  23473  cxpaddlelem  23556  cvxcl  23775  fsumharmonic  23802  ftalem5  23866  dvdsdivcl  23973  dvdsmulf1o  23986  bposlem1  24075  lgsqr  24137  lgsquad2lem2  24150  2sqlem8a  24162  2sqlem8  24163  dchrmusum2  24195  dchrvmasumiflem1  24202  dchrisum0flblem1  24209  dchrisum0lem1b  24216  pntlem3  24310  tgdim01  24414  axsegcon  24803  ax5seglem1  24804  ax5seglem2  24805  axlowdimlem6  24823  axeuclidlem  24838  axcontlem7  24846  axcontlem9  24848  axcontlem10  24849  cusgrasize2inds  25050  usgra2adedgspth  25186  vdgrun  25474  vdgrfiun  25475  vdgr1d  25476  vdgr1b  25477  vdgr1a  25479  2pthfrgra  25584  vdn1frgrav2  25598  vdgn1frgrav2  25599  frgrawopreg  25622  frrusgraord  25644  numclwwlk2lem1  25675  numclwwlk3  25682  frgrareg  25690  nmoub3i  26259  ubthlem3  26359  minvecolem2  26362  minvecolem4  26367  minvecolem5  26368  minvecolem6  26369  htthlem  26405  pjpjpre  26907  chscllem1  27125  chscllem2  27126  chscllem3  27127  cnlnadjlem2  27556  leopnmid  27626  br8d  28057  ogrpaddlt  28319  archirngz  28344  ornglmullt  28409  orngrmullt  28410  elrhmunit  28422  qqhval2lem  28624  qqhnm  28633  qqhucn  28635  esumcst  28723  esumpcvgval  28738  measunl  28877  dya2iocbrsiga  28936  dya2icobrsiga  28937  omssubadd  28961  inelcarsg  28972  carsgclctunlem2  28980  sibfof  29001  sitgaddlemb  29009  oddpwdc  29013  eulerpartlemgc  29021  bayesth  29098  erdszelem8  29709  br8  30183  totbndbnd  31825  prdsbnd  31829  rrncmslem  31868  rrntotbnd  31872  isdrngo2  31901  lsatcmp  32278  lcvexchlem2  32310  lcvexchlem3  32311  ncvr1  32547  cvrletrN  32548  cvrnbtwn3  32551  cvrnrefN  32557  cvrcmp  32558  0ltat  32566  atnle0  32584  atlen0  32585  cvlcvr1  32614  cvrval3  32687  atle  32710  athgt  32730  1cvratex  32747  ps-2  32752  ps-2b  32756  llnnleat  32787  2atneat  32789  llnle  32792  atcvrlln  32794  llncmp  32796  2llnmat  32798  2at0mat0  32799  2atm  32801  ps-2c  32802  lplnle  32814  lplnnle2at  32815  llncvrlpln2  32831  llncvrlpln  32832  2lplnmN  32833  2llnmj  32834  2atmat  32835  lplncmp  32836  lplnexllnN  32838  2llnm2N  32842  2llnm4  32844  lvolnle3at  32856  4atlem3a  32871  4atlem3b  32872  4atlem10  32880  4atlem11  32883  4atlem12  32886  lplncvrlvol2  32889  lplncvrlvol  32890  lvolcmp  32891  2lplnm2N  32895  2lplnmj  32896  dalempjsen  32927  dalemcea  32934  dalem2  32935  dalemdea  32936  dalem9  32946  dalem16  32953  dalemcjden  32966  dalem21  32968  dalem23  32970  dalem39  32985  dalem54  33000  dalem60  33006  cdlemb  33068  elpadd2at  33080  paddasslem4  33097  paddasslem7  33100  paddasslem15  33108  paddasslem16  33109  pmodlem1  33120  pmodlem2  33121  llnexchb2  33143  pclfinclN  33224  osumcllem9N  33238  pmapojoinN  33242  pexmidN  33243  pl42lem1N  33253  lhp0lt  33277  lhpexle1  33282  lhpexle2lem  33283  lhpexle3lem  33285  lhprelat3N  33314  ltrnid  33409  trlval3  33462  arglem1N  33465  cdlemc5  33470  cdleme3b  33504  cdleme3c  33505  cdleme3h  33510  cdleme7e  33522  cdleme7ga  33523  cdleme20l1  33596  cdleme20l2  33597  cdleme20l  33598  cdleme22b  33617  cdlemefrs29clN  33675  cdlemefrs32fva  33676  cdlemeg46fvcl  33782  cdlemeg46c  33789  cdlemeg46fvaw  33792  cdlemeg46req  33805  cdleme48fgv  33814  cdlemf1  33837  cdlemg1cex  33864  cdlemg2dN  33866  cdlemg2ce  33868  cdlemg12e  33923  cdlemg35  33989  cdlemh  34093  tendocan  34100  cdlemk28-3  34184  tendoex  34251  dih1  34563  dihmeetlem9N  34592  dihlspsnssN  34609  dihlspsnat  34610  lcfrlem23  34842  mzpsubst  35299  rencldnfi  35373  irrapx1  35382  pellexlem3  35385  pellexlem5  35387  infmrgelbi  35432  pellqrex  35433  pellfundge  35436  rmspecfund  35463  congtr  35521  acongeq  35539  bezoutr  35541  jm2.20nn  35558  jm2.25lem1  35559  jm2.26  35563  expdiophlem1  35582  hbtlem2  35689  suprubd  36239  suprleubrd  36246  suprlubrd  36250  suprnmpt  37061  wessf1ornlem  37082  upbdrech  37132  ssfiunibd  37136  uzfissfz  37158  xleadd2d  37159  suprltrp  37160  xleadd1d  37161  iccintsng  37209  limcrecl  37281  dvmulcncf  37369  dvdivcncf  37371  dvbdfbdioolem1  37372  ioodvbdlimc1lem2  37376  ioodvbdlimc2lem  37378  stoweidlem1  37430  stoweidlem20  37449  stoweidlem24  37453  stoweidlem34  37464  stoweidlem45  37475  stoweidlem60  37490  fourierdlem20  37558  fourierdlem31  37569  fourierdlem38  37576  fourierdlem64  37602  fourierdlem79  37617  fourierdlem94  37632  fourierdlem113  37651  fouriersw  37663  fouriercn  37664  gcdzeq  38183  pfxfv  38330  lincresunit3  39034  elbigolo1  39129
  Copyright terms: Public domain W3C validator