Theorem syl31anc 1391

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl31anc.5	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl31anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl31anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1140	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl31anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	4, 5, 6	syl2anc 593	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  syl32anc  1396  stoic4b  1797  3rspcedvdw  3599  elovmpt3rab1  7652  smo11  8330  omeulem2  8547  oeeui  8567  oaabs2  8614  omabs  8616  omxpenlem  9046  map2xp  9115  mapdom2  9116  fsuppsssupp  9324  cantnflt  9624  cnfcom  9652  mapdjuen  10134  pwsdompw  10156  ackbij1lem5  10176  cofsmo  10223  fin1a2lem4  10357  ltmul12a  12044  lt2msq1  12073  ledivp1  12091  lemul1ad  12128  lemul2ad  12129  suprubd  12151  supaddc  12156  supadd  12157  supmul1  12158  supmul  12161  rpnnen1lem3  12977  rpnnen1lem5  12979  lediv2ad  13056  xaddge0  13258  xadddi  13295  xadddi2  13297  supicc  13502  supicclub  13504  difelfznle  13644  flval3  13822  expcan  14179  ltexp2  14180  ltexp2r  14183  expubnd  14188  ltexp2rd  14258  ltexp2d  14261  leexp2d  14262  expcand  14263  hashmap  14445  swrds1  14677  ccatswrd  14679  pfxfv  14693  swrdccatin1  14735  pfxccatin12lem3  14742  cshwidxmod  14813  wrdl3s3  14972  o1fsum  15824  mertenslem1  15897  eftlub  16124  rpnnen2lem4  16232  ruclem12  16256  dvdsadd  16319  3dvds  16348  divalgmod  16423  bitsmod  16453  bitsinv1lem  16458  bezoutlem4  16559  gcdzeq  16569  rplpwr  16575  sqgcd  16579  expgcd  16580  rpmulgcd2  16673  rpdvds  16677  coprmproddvdslem  16679  isprm5  16725  divgcdodd  16728  dvdszzq  16739  divnumden  16766  crth  16796  phimullem  16797  modprm0  16824  modprmn0modprm0  16826  coprimeprodsq2  16828  pythagtriplem19  16852  pockthlem  16924  prmunb  16933  prmreclem3  16937  prmreclem6  16940  ramub  17032  ramz  17044  kerf1ghm  19270  pmtrprfv  19476  pmtrprfv3  19477  mndodcong  19565  odngen  19600  pgpfi  19628  sylow2blem3  19645  lsmless1  19683  lsmless2  19684  lsmless12  19685  lsmmod2  19699  pj1id  19722  odadd2  19872  gexexlem  19875  ablfacrplem  20090  ablfacrp  20091  ablfac1b  20095  ablfac1eu  20098  pgpfac1lem2  20100  ogrpaddlt  20161  elrhmunit  20539  rrgnz  20733  ornglmullt  20898  orngrmullt  20899  lsmssspx  21135  lspsncv0  21196  znunit  21595  uvcvvcl2  21820  uvcvv1  21821  uvcvv0  21822  coe1subfv  22309  coe1fzgsumdlem  22346  scmate  22550  mdetunilem2  22653  pmatcoe1fsupp  22741  mat2pmatlin  22775  decpmatmullem  22811  pmatcollpw1lem1  22814  pmatcollpw1lem2  22815  pm2mpghm  22856  chpscmat  22882  chp0mat  22886  chpidmat  22887  cpmadugsumlemB  22914  cpmadugsumlemC  22915  cpmadugsumlemF  22916  clsndisj  23115  neiptopnei  23172  rnelfm  23993  fmfnfmlem2  23995  fmfnfm  23998  flimss1  24013  isfcf  24074  cnextfun  24104  cnextfvval  24105  cnextf  24106  cnextcn  24107  cnextfres1  24108  ustuqtop1  24281  utopsnneiplem  24287  xblss2ps  24441  xblss2  24442  stdbdxmet  24555  metcnpi3  24586  metustexhalf  24596  nmoi  24768  nmoi2  24770  nmoco  24777  blcvx  24838  icccmplem2  24864  icccmplem3  24865  reconnlem2  24868  xrge0gsumle  24874  metds0  24891  metdstri  24892  metdseq0  24895  lebnumlem3  25005  nmoleub2lem  25156  bcthlem5  25370  csschl  25418  minveclem2  25468  minveclem3b  25470  minveclem4  25474  minveclem6  25476  icombl  25606  cncombf  25700  mbflimsup  25708  itg2monolem1  25792  itg2cnlem1  25803  itg2cnlem2  25804  bddmulibl  25881  ellimc2  25919  cpnord  25977  cpnres  25979  dvmulbr  25981  dvcobr  25988  dvlipcn  26036  dvlip2  26037  dvivthlem1  26050  lhop1lem  26055  lhop1  26056  dvfsumlem2  26069  itgsubstlem  26090  deg1add  26143  deg1sublt  26150  ply1remlem  26205  plyeq0lem  26250  taylthlem2  26414  ulmdvlem3  26442  abelthlem7  26478  pilem2  26492  pilem3  26493  pige3ALT  26562  logccv  26705  cxpaddlelem  26793  cvxcl  27026  fsumharmonic  27053  ftalem5  27118  mpodvdsmulf1o  27235  dvdsmulf1o  27237  bposlem1  27325  lgsqr  27392  lgsquad2lem2  27426  2lgsoddprmlem1  27449  2sqlem8a  27466  2sqlem8  27467  dchrmusum2  27535  dchrvmasumiflem1  27542  dchrisum0flblem1  27549  dchrisum0lem1b  27556  pntlem3  27650  noetasuplem4  27777  noetainflem4  27781  noetalem1  27782  divmulswd  28264  divsclwd  28266  uzsind  28475  tgdim01  28653  axsegcon  29074  ax5seglem1  29075  ax5seglem2  29076  axlowdimlem6  29094  axeuclidlem  29109  axcontlem7  29117  axcontlem9  29119  axcontlem10  29120  nbupgr  29491  nbumgrvtx  29493  cusgrsize2inds  29600  upgriswlk  29787  2pthnloop  29877  numclwwlk2lem1  30524  frgrreg  30542  nmoub3i  30922  ubthlem3  31021  minvecolem2  31024  minvecolem4  31029  minvecolem5  31030  minvecolem6  31031  htthlem  31066  pjpjpre  31568  chscllem1  31786  chscllem2  31787  chscllem3  31788  cnlnadjlem2  32217  leopnmid  32287  tpssad  32687  br8d  32760  swrdf1  33095  splfv3  33097  symgcom2  33225  cyc3genpmlem  33292  archirngz  33330  elrgspnlem1  33384  erld2  33408  rlocf1  33416  subrdom  33430  ricdomn1  33434  dvdsruasso  33532  unitpidl1  33571  elrspunidl  33575  qsidomlem1  33600  ssdifidlprm  33606  mxidlirredi  33620  dflringlem2  33652  1arithidomlem2  33693  1arithidom  33694  1arithufdlem3  33703  ply1gsumz  33756  mplidomlem  33785  esplymhp  33826  esplyfvaln  33832  vietadeg1  33836  lssdimle  33866  dimkerim  33885  fedgmullem2  33888  fedgmul  33889  assalactf1o  33893  fldextrspundglemul  33937  fldextrspundgdvds  33939  minplyirred  33969  irredminply  33974  algextdeglem2  33976  rtelextdg2lem  33984  constrext2chnlem  34008  constrresqrtcl  34035  2sqr3minply  34038  cos9thpiminplylem2  34041  cos9thpiminply  34046  qqhval2lem  34239  qqhnm  34248  qqhucn  34250  esumcst  34321  esumpcvgval  34336  measunl  34474  dya2iocbrsiga  34533  dya2icobrsiga  34534  omssubadd  34558  inelcarsg  34569  carsgclctunlem2  34577  sibfof  34598  sitgaddlemb  34606  oddpwdc  34612  eulerpartlemgc  34620  bayesth  34697  ftc2re  34856  breprexplemc  34890  tgoldbachgt  34921  erdszelem8  35512  2goelgoanfmla1  35738  br8  36070  matunitlindflem2  38080  totbndbnd  38252  prdsbnd  38256  rrncmslem  38295  rrntotbnd  38299  isdrngo2  38421  lsatcmp  39591  lcvexchlem2  39623  lcvexchlem3  39624  ncvr1  39860  cvrletrN  39861  cvrnbtwn3  39864  cvrnrefN  39870  cvrcmp  39871  0ltat  39879  atnle0  39897  atlen0  39898  cvlcvr1  39927  cvrval3  40001  atle  40024  athgt  40044  1cvratex  40061  ps-2  40066  ps-2b  40070  llnnleat  40101  2atneat  40103  llnle  40106  atcvrlln  40108  llncmp  40110  2llnmat  40112  2at0mat0  40113  2atm  40115  ps-2c  40116  lplnle  40128  lplnnle2at  40129  llncvrlpln2  40145  llncvrlpln  40146  2lplnmN  40147  2llnmj  40148  2atmat  40149  lplncmp  40150  lplnexllnN  40152  2llnm2N  40156  2llnm4  40158  lvolnle3at  40170  4atlem3a  40185  4atlem3b  40186  4atlem10  40194  4atlem11  40197  4atlem12  40200  lplncvrlvol2  40203  lplncvrlvol  40204  lvolcmp  40205  2lplnm2N  40209  2lplnmj  40210  dalempjsen  40241  dalemcea  40248  dalem2  40249  dalemdea  40250  dalem9  40260  dalem16  40267  dalemcjden  40280  dalem21  40282  dalem23  40284  dalem39  40299  dalem54  40314  dalem60  40320  cdlemb  40382  elpadd2at  40394  paddasslem4  40411  paddasslem7  40414  paddasslem15  40422  paddasslem16  40423  pmodlem1  40434  pmodlem2  40435  llnexchb2  40457  pclfinclN  40538  osumcllem9N  40552  pmapojoinN  40556  pexmidN  40557  pl42lem1N  40567  lhp0lt  40591  lhpexle1  40596  lhpexle2lem  40597  lhpexle3lem  40599  lhprelat3N  40628  ltrnid  40723  trlval3  40775  arglem1N  40778  cdlemc5  40783  cdleme3b  40817  cdleme3c  40818  cdleme3h  40823  cdleme7e  40835  cdleme7ga  40836  cdleme20l1  40908  cdleme20l2  40909  cdleme20l  40910  cdleme22b  40929  cdlemefrs29clN  40987  cdlemefrs32fva  40988  cdlemeg46fvcl  41094  cdlemeg46c  41101  cdlemeg46fvaw  41104  cdlemeg46req  41117  cdleme48fgv  41126  cdlemf1  41149  cdlemg1cex  41176  cdlemg2dN  41178  cdlemg2ce  41180  cdlemg12e  41235  cdlemg35  41301  cdlemh  41405  tendocan  41412  cdlemk28-3  41496  tendoex  41563  dih1  41874  dihmeetlem9N  41903  dihlspsnssN  41920  dihlspsnat  41921  lcfrlem23  42153  renegneg  42985  fsuppind  43136  flt4lem4  43195  3cubes  43235  mzpsubst  43293  rencldnfi  43362  irrapx1  43369  pellexlem3  43372  pellexlem5  43374  infmrgelbi  43419  pellqrex  43420  pellfundge  43423  rmspecfund  43450  congtr  43506  acongeq  43524  jm2.20nn  43538  jm2.25lem1  43539  jm2.26  43543  expdiophlem1  43562  hbtlem2  43665  cantnftermord  43861  suprleubrd  44706  suprlubrd  44708  suprnmpt  45716  wessf1ornlem  45727  mpct  45742  upbdrech  45848  ssfiunibd  45852  uzfissfz  45866  xleadd2d  45867  suprltrp  45868  xleadd1d  45869  suprleubrnmpt  45960  iccintsng  46063  limcrecl  46169  fnlimfvre  46212  dvmulcncf  46463  dvdivcncf  46465  dvbdfbdioolem1  46466  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  stoweidlem1  46539  stoweidlem20  46558  stoweidlem24  46562  stoweidlem34  46572  stoweidlem45  46583  stoweidlem60  46598  fourierdlem20  46665  fourierdlem31  46676  fourierdlem38  46683  fourierdlem64  46708  fourierdlem79  46723  fourierdlem94  46738  fourierdlem113  46757  fouriersw  46769  fouriercn  46770  sge0isum  46965  hoicvr  47086  ovnsubaddlem2  47109  hoidmv1lelem1  47129  hoidmv1lelem3  47131  hoidmvlelem1  47133  hoidmvlelem4  47136  smflimlem2  47310  2timesltsq  47936  fmtnof1  48108  lighneallem2  48179  uspgrlim  48578  upgrwlkupwlk  48726  lincresunit3  49067  elbigolo1  49143  eenglngeehlnm  49325