Theorem syl31anc 1370

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 1125	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl31anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	4, 5, 6	syl2anc 582	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  syl32anc  1375  stoic4b  1772  elovmpt3rab1  7681  smo11  8385  omeulem2  8604  oeeui  8623  oaabs2  8670  omabs  8672  omxpenlem  9098  map2xp  9172  mapdom2  9173  fsuppsssupp  9406  cantnflt  9697  cnfcom  9725  mapdjuen  10205  pwsdompw  10229  ackbij1lem5  10249  cofsmo  10294  fin1a2lem4  10428  ltmul12a  12103  lt2msq1  12131  ledivp1  12149  lemul1ad  12186  lemul2ad  12187  suprubd  12209  supaddc  12214  supadd  12215  supmul1  12216  supmul  12219  rpnnen1lem3  12996  rpnnen1lem5  12998  lediv2ad  13073  xaddge0  13272  xadddi  13309  xadddi2  13311  supicc  13513  supicclub  13515  difelfznle  13650  flval3  13816  expcan  14169  ltexp2  14170  ltexp2r  14173  expubnd  14177  ltexp2rd  14246  ltexp2d  14249  leexp2d  14250  expcand  14251  hashmap  14430  swrds1  14652  ccatswrd  14654  pfxfv  14668  swrdccatin1  14711  pfxccatin12lem3  14718  cshwidxmod  14789  wrdl3s3  14949  o1fsum  15795  mertenslem1  15866  eftlub  16089  rpnnen2lem4  16197  ruclem12  16221  dvdsadd  16282  3dvds  16311  divalgmod  16386  bitsmod  16414  bitsinv1lem  16419  bezoutlem4  16521  gcdzeq  16531  rplpwr  16536  sqgcd  16539  rpmulgcd2  16630  rpdvds  16634  coprmproddvdslem  16636  isprm5  16681  divgcdodd  16684  dvdszzq  16696  divnumden  16723  crth  16750  phimullem  16751  modprm0  16777  modprmn0modprm0  16779  coprimeprodsq2  16781  pythagtriplem19  16805  pockthlem  16877  prmunb  16886  prmreclem3  16890  prmreclem6  16893  ramub  16985  ramz  16997  kerf1ghm  19210  pmtrprfv  19420  pmtrprfv3  19421  mndodcong  19509  odngen  19544  pgpfi  19572  sylow2blem3  19589  lsmless1  19627  lsmless2  19628  lsmless12  19629  lsmmod2  19643  pj1id  19666  odadd2  19816  gexexlem  19819  ablfacrplem  20034  ablfacrp  20035  ablfac1b  20039  ablfac1eu  20042  pgpfac1lem2  20044  elrhmunit  20461  lsmssspx  20985  lspsncv0  21046  znunit  21514  uvcvvcl2  21739  uvcvv1  21740  uvcvv0  21741  coe1subfv  22210  coe1fzgsumdlem  22247  scmate  22456  mdetunilem2  22559  pmatcoe1fsupp  22647  mat2pmatlin  22681  decpmatmullem  22717  pmatcollpw1lem1  22720  pmatcollpw1lem2  22721  pm2mpghm  22762  chpscmat  22788  chp0mat  22792  chpidmat  22793  cpmadugsumlemB  22820  cpmadugsumlemC  22821  cpmadugsumlemF  22822  clsndisj  23023  neiptopnei  23080  rnelfm  23901  fmfnfmlem2  23903  fmfnfm  23906  flimss1  23921  isfcf  23982  cnextfun  24012  cnextfvval  24013  cnextf  24014  cnextcn  24015  cnextfres1  24016  ustuqtop1  24190  utopsnneiplem  24196  xblss2ps  24351  xblss2  24352  stdbdxmet  24468  metcnpi3  24499  metustexhalf  24509  nmoi  24689  nmoi2  24691  nmoco  24698  blcvx  24758  icccmplem2  24783  icccmplem3  24784  reconnlem2  24787  xrge0gsumle  24793  metds0  24810  metdstri  24811  metdseq0  24814  lebnumlem3  24933  nmoleub2lem  25085  bcthlem5  25300  csschl  25348  minveclem2  25398  minveclem3b  25400  minveclem4  25404  minveclem6  25406  icombl  25537  cncombf  25631  mbflimsup  25639  itg2monolem1  25724  itg2cnlem1  25735  itg2cnlem2  25736  bddmulibl  25812  ellimc2  25850  cpnord  25909  cpnres  25911  dvmulbr  25913  dvmulbrOLD  25914  dvcobr  25921  dvcobrOLD  25922  dvlipcn  25971  dvlip2  25972  dvivthlem1  25985  lhop1lem  25990  lhop1  25991  dvfsumlem2  26005  dvfsumlem2OLD  26006  itgsubstlem  26027  deg1add  26083  deg1sublt  26090  ply1remlem  26144  plyeq0lem  26189  taylthlem2  26354  taylthlem2OLD  26355  ulmdvlem3  26383  abelthlem7  26420  pilem2  26434  pilem3  26435  pige3ALT  26499  logccv  26642  cxpaddlelem  26731  cvxcl  26962  fsumharmonic  26989  ftalem5  27054  mpodvdsmulf1o  27171  dvdsmulf1o  27173  bposlem1  27262  lgsqr  27329  lgsquad2lem2  27363  2lgsoddprmlem1  27386  2sqlem8a  27403  2sqlem8  27404  dchrmusum2  27472  dchrvmasumiflem1  27479  dchrisum0flblem1  27486  dchrisum0lem1b  27493  pntlem3  27587  noetasuplem4  27715  noetainflem4  27719  noetalem1  27720  divsmulwd  28143  divsclwd  28145  tgdim01  28383  axsegcon  28810  ax5seglem1  28811  ax5seglem2  28812  axlowdimlem6  28830  axeuclidlem  28845  axcontlem7  28853  axcontlem9  28855  axcontlem10  28856  nbupgr  29229  nbumgrvtx  29231  cusgrsize2inds  29339  upgriswlk  29527  2pthnloop  29617  numclwwlk2lem1  30258  frgrreg  30276  nmoub3i  30655  ubthlem3  30754  minvecolem2  30757  minvecolem4  30762  minvecolem5  30763  minvecolem6  30764  htthlem  30799  pjpjpre  31301  chscllem1  31519  chscllem2  31520  chscllem3  31521  cnlnadjlem2  31950  leopnmid  32020  br8d  32479  swrdf1  32766  splfv3  32768  ogrpaddlt  32887  symgcom2  32897  cyc3genpmlem  32964  archirngz  32989  rlocf1  33063  rrgnz  33070  subrdom  33073  ornglmullt  33121  orngrmullt  33122  dvdsruasso  33197  unitpidl1  33236  elrspunidl  33240  qsidomlem1  33264  ssdifidlprm  33270  mxidlirredi  33283  1arithidomlem2  33348  1arithidom  33349  1arithufdlem3  33361  ply1gsumz  33400  lssdimle  33436  dimkerim  33456  fedgmullem2  33459  fedgmul  33460  minplyirred  33512  irredminply  33515  algextdeglem2  33517  qqhval2lem  33713  qqhnm  33722  qqhucn  33724  esumcst  33813  esumpcvgval  33828  measunl  33966  dya2iocbrsiga  34026  dya2icobrsiga  34027  omssubadd  34051  inelcarsg  34062  carsgclctunlem2  34070  sibfof  34091  sitgaddlemb  34099  oddpwdc  34105  eulerpartlemgc  34113  bayesth  34190  ftc2re  34361  breprexplemc  34395  tgoldbachgt  34426  erdszelem8  34939  2goelgoanfmla1  35165  br8  35481  matunitlindflem2  37221  totbndbnd  37393  prdsbnd  37397  rrncmslem  37436  rrntotbnd  37440  isdrngo2  37562  lsatcmp  38605  lcvexchlem2  38637  lcvexchlem3  38638  ncvr1  38874  cvrletrN  38875  cvrnbtwn3  38878  cvrnrefN  38884  cvrcmp  38885  0ltat  38893  atnle0  38911  atlen0  38912  cvlcvr1  38941  cvrval3  39016  atle  39039  athgt  39059  1cvratex  39076  ps-2  39081  ps-2b  39085  llnnleat  39116  2atneat  39118  llnle  39121  atcvrlln  39123  llncmp  39125  2llnmat  39127  2at0mat0  39128  2atm  39130  ps-2c  39131  lplnle  39143  lplnnle2at  39144  llncvrlpln2  39160  llncvrlpln  39161  2lplnmN  39162  2llnmj  39163  2atmat  39164  lplncmp  39165  lplnexllnN  39167  2llnm2N  39171  2llnm4  39173  lvolnle3at  39185  4atlem3a  39200  4atlem3b  39201  4atlem10  39209  4atlem11  39212  4atlem12  39215  lplncvrlvol2  39218  lplncvrlvol  39219  lvolcmp  39220  2lplnm2N  39224  2lplnmj  39225  dalempjsen  39256  dalemcea  39263  dalem2  39264  dalemdea  39265  dalem9  39275  dalem16  39282  dalemcjden  39295  dalem21  39297  dalem23  39299  dalem39  39314  dalem54  39329  dalem60  39335  cdlemb  39397  elpadd2at  39409  paddasslem4  39426  paddasslem7  39429  paddasslem15  39437  paddasslem16  39438  pmodlem1  39449  pmodlem2  39450  llnexchb2  39472  pclfinclN  39553  osumcllem9N  39567  pmapojoinN  39571  pexmidN  39572  pl42lem1N  39582  lhp0lt  39606  lhpexle1  39611  lhpexle2lem  39612  lhpexle3lem  39614  lhprelat3N  39643  ltrnid  39738  trlval3  39790  arglem1N  39793  cdlemc5  39798  cdleme3b  39832  cdleme3c  39833  cdleme3h  39838  cdleme7e  39850  cdleme7ga  39851  cdleme20l1  39923  cdleme20l2  39924  cdleme20l  39925  cdleme22b  39944  cdlemefrs29clN  40002  cdlemefrs32fva  40003  cdlemeg46fvcl  40109  cdlemeg46c  40116  cdlemeg46fvaw  40119  cdlemeg46req  40132  cdleme48fgv  40141  cdlemf1  40164  cdlemg1cex  40191  cdlemg2dN  40193  cdlemg2ce  40195  cdlemg12e  40250  cdlemg35  40316  cdlemh  40420  tendocan  40427  cdlemk28-3  40511  tendoex  40578  dih1  40889  dihmeetlem9N  40918  dihlspsnssN  40935  dihlspsnat  40936  lcfrlem23  41168  3rspcedvdw  41836  fsuppind  41958  expgcd  42029  renegneg  42101  flt4lem4  42208  3cubes  42252  mzpsubst  42310  rencldnfi  42383  irrapx1  42390  pellexlem3  42393  pellexlem5  42395  infmrgelbi  42440  pellqrex  42441  pellfundge  42444  rmspecfund  42471  congtr  42528  acongeq  42546  jm2.20nn  42560  jm2.25lem1  42561  jm2.26  42565  expdiophlem1  42584  hbtlem2  42690  cantnftermord  42891  suprleubrd  43738  suprlubrd  43740  suprnmpt  44686  wessf1ornlem  44697  mpct  44713  upbdrech  44825  ssfiunibd  44829  uzfissfz  44846  xleadd2d  44847  suprltrp  44848  xleadd1d  44849  suprleubrnmpt  44942  iccintsng  45046  limcrecl  45155  fnlimfvre  45200  dvmulcncf  45451  dvdivcncf  45453  dvbdfbdioolem1  45454  ioodvbdlimc1lem2  45458  ioodvbdlimc2lem  45460  stoweidlem1  45527  stoweidlem20  45546  stoweidlem24  45550  stoweidlem34  45560  stoweidlem45  45571  stoweidlem60  45586  fourierdlem20  45653  fourierdlem31  45664  fourierdlem38  45671  fourierdlem64  45696  fourierdlem79  45711  fourierdlem94  45726  fourierdlem113  45745  fouriersw  45757  fouriercn  45758  sge0isum  45953  hoicvr  46074  ovnsubaddlem2  46097  hoidmv1lelem1  46117  hoidmv1lelem3  46119  hoidmvlelem1  46121  hoidmvlelem4  46124  smflimlem2  46298  fmtnof1  47012  lighneallem2  47083  upgrwlkupwlk  47388  lincresunit3  47735  elbigolo1  47816  eenglngeehlnm  47998