Theorem syl31anc 1376

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl32anc  1381  stoic4b  1780  3rspcedvdw  3583  elovmpt3rab1  7618  smo11  8295  omeulem2  8509  oeeui  8529  oaabs2  8576  omabs  8578  omxpenlem  9007  map2xp  9076  mapdom2  9077  fsuppsssupp  9285  cantnflt  9582  cnfcom  9610  mapdjuen  10092  pwsdompw  10114  ackbij1lem5  10134  cofsmo  10180  fin1a2lem4  10314  ltmul12a  11998  lt2msq1  12027  ledivp1  12045  lemul1ad  12082  lemul2ad  12083  suprubd  12105  supaddc  12110  supadd  12111  supmul1  12112  supmul  12115  rpnnen1lem3  12893  rpnnen1lem5  12895  lediv2ad  12972  xaddge0  13174  xadddi  13211  xadddi2  13213  supicc  13418  supicclub  13420  difelfznle  13559  flval3  13736  expcan  14093  ltexp2  14094  ltexp2r  14097  expubnd  14102  ltexp2rd  14172  ltexp2d  14175  leexp2d  14176  expcand  14177  hashmap  14359  swrds1  14591  ccatswrd  14593  pfxfv  14607  swrdccatin1  14649  pfxccatin12lem3  14656  cshwidxmod  14727  wrdl3s3  14886  o1fsum  15737  mertenslem1  15808  eftlub  16035  rpnnen2lem4  16143  ruclem12  16167  dvdsadd  16230  3dvds  16259  divalgmod  16334  bitsmod  16364  bitsinv1lem  16369  bezoutlem4  16470  gcdzeq  16480  rplpwr  16486  sqgcd  16490  expgcd  16491  rpmulgcd2  16584  rpdvds  16588  coprmproddvdslem  16590  isprm5  16635  divgcdodd  16638  dvdszzq  16649  divnumden  16676  crth  16706  phimullem  16707  modprm0  16734  modprmn0modprm0  16736  coprimeprodsq2  16738  pythagtriplem19  16762  pockthlem  16834  prmunb  16843  prmreclem3  16847  prmreclem6  16850  ramub  16942  ramz  16954  kerf1ghm  19180  pmtrprfv  19386  pmtrprfv3  19387  mndodcong  19475  odngen  19510  pgpfi  19538  sylow2blem3  19555  lsmless1  19593  lsmless2  19594  lsmless12  19595  lsmmod2  19609  pj1id  19632  odadd2  19782  gexexlem  19785  ablfacrplem  20000  ablfacrp  20001  ablfac1b  20005  ablfac1eu  20008  pgpfac1lem2  20010  ogrpaddlt  20071  elrhmunit  20445  rrgnz  20639  ornglmullt  20804  orngrmullt  20805  lsmssspx  21042  lspsncv0  21103  znunit  21520  uvcvvcl2  21745  uvcvv1  21746  uvcvv0  21747  coe1subfv  22209  coe1fzgsumdlem  22246  scmate  22453  mdetunilem2  22556  pmatcoe1fsupp  22644  mat2pmatlin  22678  decpmatmullem  22714  pmatcollpw1lem1  22717  pmatcollpw1lem2  22718  pm2mpghm  22759  chpscmat  22785  chp0mat  22789  chpidmat  22790  cpmadugsumlemB  22817  cpmadugsumlemC  22818  cpmadugsumlemF  22819  clsndisj  23018  neiptopnei  23075  rnelfm  23896  fmfnfmlem2  23898  fmfnfm  23901  flimss1  23916  isfcf  23977  cnextfun  24007  cnextfvval  24008  cnextf  24009  cnextcn  24010  cnextfres1  24011  ustuqtop1  24184  utopsnneiplem  24190  xblss2ps  24344  xblss2  24345  stdbdxmet  24458  metcnpi3  24489  metustexhalf  24499  nmoi  24671  nmoi2  24673  nmoco  24680  blcvx  24741  icccmplem2  24767  icccmplem3  24768  reconnlem2  24771  xrge0gsumle  24777  metds0  24794  metdstri  24795  metdseq0  24798  lebnumlem3  24908  nmoleub2lem  25059  bcthlem5  25273  csschl  25321  minveclem2  25371  minveclem3b  25373  minveclem4  25377  minveclem6  25379  icombl  25509  cncombf  25603  mbflimsup  25611  itg2monolem1  25695  itg2cnlem1  25706  itg2cnlem2  25707  bddmulibl  25784  ellimc2  25822  cpnord  25880  cpnres  25882  dvmulbr  25884  dvcobr  25891  dvlipcn  25940  dvlip2  25941  dvivthlem1  25954  lhop1lem  25959  lhop1  25960  dvfsumlem2  25974  dvfsumlem2OLD  25975  itgsubstlem  25996  deg1add  26049  deg1sublt  26056  ply1remlem  26111  plyeq0lem  26156  taylthlem2  26322  taylthlem2OLD  26323  ulmdvlem3  26351  abelthlem7  26388  pilem2  26402  pilem3  26403  pige3ALT  26469  logccv  26612  cxpaddlelem  26701  cvxcl  26935  fsumharmonic  26962  ftalem5  27027  mpodvdsmulf1o  27144  dvdsmulf1o  27146  bposlem1  27235  lgsqr  27302  lgsquad2lem2  27336  2lgsoddprmlem1  27359  2sqlem8a  27376  2sqlem8  27377  dchrmusum2  27445  dchrvmasumiflem1  27452  dchrisum0flblem1  27459  dchrisum0lem1b  27466  pntlem3  27560  noetasuplem4  27688  noetainflem4  27692  noetalem1  27693  divmulswd  28174  divsclwd  28176  uzsind  28385  tgdim01  28563  axsegcon  28984  ax5seglem1  28985  ax5seglem2  28986  axlowdimlem6  29004  axeuclidlem  29019  axcontlem7  29027  axcontlem9  29029  axcontlem10  29030  nbupgr  29401  nbumgrvtx  29403  cusgrsize2inds  29511  upgriswlk  29698  2pthnloop  29788  numclwwlk2lem1  30435  frgrreg  30453  nmoub3i  30833  ubthlem3  30932  minvecolem2  30935  minvecolem4  30940  minvecolem5  30941  minvecolem6  30942  htthlem  30977  pjpjpre  31479  chscllem1  31697  chscllem2  31698  chscllem3  31699  cnlnadjlem2  32128  leopnmid  32198  tpssad  32598  br8d  32670  swrdf1  33021  splfv3  33023  symgcom2  33150  cyc3genpmlem  33217  archirngz  33255  elrgspnlem1  33308  rlocf1  33339  subrdom  33351  dvdsruasso  33450  unitpidl1  33489  elrspunidl  33493  qsidomlem1  33517  ssdifidlprm  33523  mxidlirredi  33536  1arithidomlem2  33601  1arithidom  33602  1arithufdlem3  33611  ply1gsumz  33664  esplymhp  33717  esplyfvaln  33723  vietadeg1  33727  lssdimle  33757  dimkerim  33777  fedgmullem2  33780  fedgmul  33781  assalactf1o  33785  fldextrspundglemul  33829  fldextrspundgdvds  33831  minplyirred  33861  irredminply  33866  algextdeglem2  33868  rtelextdg2lem  33876  constrext2chnlem  33900  constrresqrtcl  33927  2sqr3minply  33930  cos9thpiminplylem2  33933  cos9thpiminply  33938  qqhval2lem  34131  qqhnm  34140  qqhucn  34142  esumcst  34213  esumpcvgval  34228  measunl  34366  dya2iocbrsiga  34425  dya2icobrsiga  34426  omssubadd  34450  inelcarsg  34461  carsgclctunlem2  34469  sibfof  34490  sitgaddlemb  34498  oddpwdc  34504  eulerpartlemgc  34512  bayesth  34589  ftc2re  34748  breprexplemc  34782  tgoldbachgt  34813  erdszelem8  35386  2goelgoanfmla1  35612  br8  35944  matunitlindflem2  37929  totbndbnd  38101  prdsbnd  38105  rrncmslem  38144  rrntotbnd  38148  isdrngo2  38270  lsatcmp  39440  lcvexchlem2  39472  lcvexchlem3  39473  ncvr1  39709  cvrletrN  39710  cvrnbtwn3  39713  cvrnrefN  39719  cvrcmp  39720  0ltat  39728  atnle0  39746  atlen0  39747  cvlcvr1  39776  cvrval3  39850  atle  39873  athgt  39893  1cvratex  39910  ps-2  39915  ps-2b  39919  llnnleat  39950  2atneat  39952  llnle  39955  atcvrlln  39957  llncmp  39959  2llnmat  39961  2at0mat0  39962  2atm  39964  ps-2c  39965  lplnle  39977  lplnnle2at  39978  llncvrlpln2  39994  llncvrlpln  39995  2lplnmN  39996  2llnmj  39997  2atmat  39998  lplncmp  39999  lplnexllnN  40001  2llnm2N  40005  2llnm4  40007  lvolnle3at  40019  4atlem3a  40034  4atlem3b  40035  4atlem10  40043  4atlem11  40046  4atlem12  40049  lplncvrlvol2  40052  lplncvrlvol  40053  lvolcmp  40054  2lplnm2N  40058  2lplnmj  40059  dalempjsen  40090  dalemcea  40097  dalem2  40098  dalemdea  40099  dalem9  40109  dalem16  40116  dalemcjden  40129  dalem21  40131  dalem23  40133  dalem39  40148  dalem54  40163  dalem60  40169  cdlemb  40231  elpadd2at  40243  paddasslem4  40260  paddasslem7  40263  paddasslem15  40271  paddasslem16  40272  pmodlem1  40283  pmodlem2  40284  llnexchb2  40306  pclfinclN  40387  osumcllem9N  40401  pmapojoinN  40405  pexmidN  40406  pl42lem1N  40416  lhp0lt  40440  lhpexle1  40445  lhpexle2lem  40446  lhpexle3lem  40448  lhprelat3N  40477  ltrnid  40572  trlval3  40624  arglem1N  40627  cdlemc5  40632  cdleme3b  40666  cdleme3c  40667  cdleme3h  40672  cdleme7e  40684  cdleme7ga  40685  cdleme20l1  40757  cdleme20l2  40758  cdleme20l  40759  cdleme22b  40778  cdlemefrs29clN  40836  cdlemefrs32fva  40837  cdlemeg46fvcl  40943  cdlemeg46c  40950  cdlemeg46fvaw  40953  cdlemeg46req  40966  cdleme48fgv  40975  cdlemf1  40998  cdlemg1cex  41025  cdlemg2dN  41027  cdlemg2ce  41029  cdlemg12e  41084  cdlemg35  41150  cdlemh  41254  tendocan  41261  cdlemk28-3  41345  tendoex  41412  dih1  41723  dihmeetlem9N  41752  dihlspsnssN  41769  dihlspsnat  41770  lcfrlem23  42002  renegneg  42843  fsuppind  43022  flt4lem4  43081  3cubes  43121  mzpsubst  43179  rencldnfi  43252  irrapx1  43259  pellexlem3  43262  pellexlem5  43264  infmrgelbi  43309  pellqrex  43310  pellfundge  43313  rmspecfund  43340  congtr  43396  acongeq  43414  jm2.20nn  43428  jm2.25lem1  43429  jm2.26  43433  expdiophlem1  43452  hbtlem2  43555  cantnftermord  43751  suprleubrd  44596  suprlubrd  44598  suprnmpt  45607  wessf1ornlem  45618  mpct  45633  upbdrech  45741  ssfiunibd  45745  uzfissfz  45759  xleadd2d  45760  suprltrp  45761  xleadd1d  45762  suprleubrnmpt  45854  iccintsng  45957  limcrecl  46063  fnlimfvre  46106  dvmulcncf  46357  dvdivcncf  46359  dvbdfbdioolem1  46360  ioodvbdlimc1lem2  46364  ioodvbdlimc2lem  46366  stoweidlem1  46433  stoweidlem20  46452  stoweidlem24  46456  stoweidlem34  46466  stoweidlem45  46477  stoweidlem60  46492  fourierdlem20  46559  fourierdlem31  46570  fourierdlem38  46577  fourierdlem64  46602  fourierdlem79  46617  fourierdlem94  46632  fourierdlem113  46651  fouriersw  46663  fouriercn  46664  sge0isum  46859  hoicvr  46980  ovnsubaddlem2  47003  hoidmv1lelem1  47023  hoidmv1lelem3  47025  hoidmvlelem1  47027  hoidmvlelem4  47030  smflimlem2  47204  fmtnof1  47969  lighneallem2  48040  uspgrlim  48426  upgrwlkupwlk  48574  lincresunit3  48915  elbigolo1  48991  eenglngeehlnm  49173