Theorem syl31anc 1375

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

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

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 1088

This theorem is referenced by:  syl32anc  1380  stoic4b  1779  3rspcedvdw  3595  elovmpt3rab1  7606  smo11  8284  omeulem2  8498  oeeui  8517  oaabs2  8564  omabs  8566  omxpenlem  8991  map2xp  9060  mapdom2  9061  fsuppsssupp  9265  cantnflt  9562  cnfcom  9590  mapdjuen  10069  pwsdompw  10091  ackbij1lem5  10111  cofsmo  10157  fin1a2lem4  10291  ltmul12a  11974  lt2msq1  12003  ledivp1  12021  lemul1ad  12058  lemul2ad  12059  suprubd  12081  supaddc  12086  supadd  12087  supmul1  12088  supmul  12091  rpnnen1lem3  12874  rpnnen1lem5  12876  lediv2ad  12953  xaddge0  13154  xadddi  13191  xadddi2  13193  supicc  13398  supicclub  13400  difelfznle  13539  flval3  13716  expcan  14073  ltexp2  14074  ltexp2r  14077  expubnd  14082  ltexp2rd  14152  ltexp2d  14155  leexp2d  14156  expcand  14157  hashmap  14339  swrds1  14571  ccatswrd  14573  pfxfv  14587  swrdccatin1  14629  pfxccatin12lem3  14636  cshwidxmod  14707  wrdl3s3  14866  o1fsum  15717  mertenslem1  15788  eftlub  16015  rpnnen2lem4  16123  ruclem12  16147  dvdsadd  16210  3dvds  16239  divalgmod  16314  bitsmod  16344  bitsinv1lem  16349  bezoutlem4  16450  gcdzeq  16460  rplpwr  16466  sqgcd  16470  expgcd  16471  rpmulgcd2  16564  rpdvds  16568  coprmproddvdslem  16570  isprm5  16615  divgcdodd  16618  dvdszzq  16629  divnumden  16656  crth  16686  phimullem  16687  modprm0  16714  modprmn0modprm0  16716  coprimeprodsq2  16718  pythagtriplem19  16742  pockthlem  16814  prmunb  16823  prmreclem3  16827  prmreclem6  16830  ramub  16922  ramz  16934  kerf1ghm  19157  pmtrprfv  19363  pmtrprfv3  19364  mndodcong  19452  odngen  19487  pgpfi  19515  sylow2blem3  19532  lsmless1  19570  lsmless2  19571  lsmless12  19572  lsmmod2  19586  pj1id  19609  odadd2  19759  gexexlem  19762  ablfacrplem  19977  ablfacrp  19978  ablfac1b  19982  ablfac1eu  19985  pgpfac1lem2  19987  ogrpaddlt  20048  elrhmunit  20423  rrgnz  20617  ornglmullt  20782  orngrmullt  20783  lsmssspx  21020  lspsncv0  21081  znunit  21498  uvcvvcl2  21723  uvcvv1  21724  uvcvv0  21725  coe1subfv  22178  coe1fzgsumdlem  22216  scmate  22423  mdetunilem2  22526  pmatcoe1fsupp  22614  mat2pmatlin  22648  decpmatmullem  22684  pmatcollpw1lem1  22687  pmatcollpw1lem2  22688  pm2mpghm  22729  chpscmat  22755  chp0mat  22759  chpidmat  22760  cpmadugsumlemB  22787  cpmadugsumlemC  22788  cpmadugsumlemF  22789  clsndisj  22988  neiptopnei  23045  rnelfm  23866  fmfnfmlem2  23868  fmfnfm  23871  flimss1  23886  isfcf  23947  cnextfun  23977  cnextfvval  23978  cnextf  23979  cnextcn  23980  cnextfres1  23981  ustuqtop1  24154  utopsnneiplem  24160  xblss2ps  24314  xblss2  24315  stdbdxmet  24428  metcnpi3  24459  metustexhalf  24469  nmoi  24641  nmoi2  24643  nmoco  24650  blcvx  24711  icccmplem2  24737  icccmplem3  24738  reconnlem2  24741  xrge0gsumle  24747  metds0  24764  metdstri  24765  metdseq0  24768  lebnumlem3  24887  nmoleub2lem  25039  bcthlem5  25253  csschl  25301  minveclem2  25351  minveclem3b  25353  minveclem4  25357  minveclem6  25359  icombl  25490  cncombf  25584  mbflimsup  25592  itg2monolem1  25676  itg2cnlem1  25687  itg2cnlem2  25688  bddmulibl  25765  ellimc2  25803  cpnord  25862  cpnres  25864  dvmulbr  25866  dvmulbrOLD  25867  dvcobr  25874  dvcobrOLD  25875  dvlipcn  25924  dvlip2  25925  dvivthlem1  25938  lhop1lem  25943  lhop1  25944  dvfsumlem2  25958  dvfsumlem2OLD  25959  itgsubstlem  25980  deg1add  26033  deg1sublt  26040  ply1remlem  26095  plyeq0lem  26140  taylthlem2  26307  taylthlem2OLD  26308  ulmdvlem3  26336  abelthlem7  26373  pilem2  26387  pilem3  26388  pige3ALT  26454  logccv  26597  cxpaddlelem  26686  cvxcl  26920  fsumharmonic  26947  ftalem5  27012  mpodvdsmulf1o  27129  dvdsmulf1o  27131  bposlem1  27220  lgsqr  27287  lgsquad2lem2  27321  2lgsoddprmlem1  27344  2sqlem8a  27361  2sqlem8  27362  dchrmusum2  27430  dchrvmasumiflem1  27437  dchrisum0flblem1  27444  dchrisum0lem1b  27451  pntlem3  27545  noetasuplem4  27673  noetainflem4  27677  noetalem1  27678  divsmulwd  28131  divsclwd  28133  uzsind  28327  tgdim01  28483  axsegcon  28903  ax5seglem1  28904  ax5seglem2  28905  axlowdimlem6  28923  axeuclidlem  28938  axcontlem7  28946  axcontlem9  28948  axcontlem10  28949  nbupgr  29320  nbumgrvtx  29322  cusgrsize2inds  29430  upgriswlk  29617  2pthnloop  29707  numclwwlk2lem1  30351  frgrreg  30369  nmoub3i  30748  ubthlem3  30847  minvecolem2  30850  minvecolem4  30855  minvecolem5  30856  minvecolem6  30857  htthlem  30892  pjpjpre  31394  chscllem1  31612  chscllem2  31613  chscllem3  31614  cnlnadjlem2  32043  leopnmid  32113  tpssad  32514  br8d  32586  swrdf1  32932  splfv3  32934  symgcom2  33048  cyc3genpmlem  33115  archirngz  33153  elrgspnlem1  33204  rlocf1  33235  subrdom  33246  dvdsruasso  33345  unitpidl1  33384  elrspunidl  33388  qsidomlem1  33412  ssdifidlprm  33418  mxidlirredi  33431  1arithidomlem2  33496  1arithidom  33497  1arithufdlem3  33506  ply1gsumz  33554  esplymhp  33584  lssdimle  33615  dimkerim  33635  fedgmullem2  33638  fedgmul  33639  assalactf1o  33643  fldextrspundglemul  33687  fldextrspundgdvds  33689  minplyirred  33719  irredminply  33724  algextdeglem2  33726  rtelextdg2lem  33734  constrext2chnlem  33758  constrresqrtcl  33785  2sqr3minply  33788  cos9thpiminplylem2  33791  cos9thpiminply  33796  qqhval2lem  33989  qqhnm  33998  qqhucn  34000  esumcst  34071  esumpcvgval  34086  measunl  34224  dya2iocbrsiga  34283  dya2icobrsiga  34284  omssubadd  34308  inelcarsg  34319  carsgclctunlem2  34327  sibfof  34348  sitgaddlemb  34356  oddpwdc  34362  eulerpartlemgc  34370  bayesth  34447  ftc2re  34606  breprexplemc  34640  tgoldbachgt  34671  erdszelem8  35230  2goelgoanfmla1  35456  br8  35788  matunitlindflem2  37656  totbndbnd  37828  prdsbnd  37832  rrncmslem  37871  rrntotbnd  37875  isdrngo2  37997  lsatcmp  39041  lcvexchlem2  39073  lcvexchlem3  39074  ncvr1  39310  cvrletrN  39311  cvrnbtwn3  39314  cvrnrefN  39320  cvrcmp  39321  0ltat  39329  atnle0  39347  atlen0  39348  cvlcvr1  39377  cvrval3  39451  atle  39474  athgt  39494  1cvratex  39511  ps-2  39516  ps-2b  39520  llnnleat  39551  2atneat  39553  llnle  39556  atcvrlln  39558  llncmp  39560  2llnmat  39562  2at0mat0  39563  2atm  39565  ps-2c  39566  lplnle  39578  lplnnle2at  39579  llncvrlpln2  39595  llncvrlpln  39596  2lplnmN  39597  2llnmj  39598  2atmat  39599  lplncmp  39600  lplnexllnN  39602  2llnm2N  39606  2llnm4  39608  lvolnle3at  39620  4atlem3a  39635  4atlem3b  39636  4atlem10  39644  4atlem11  39647  4atlem12  39650  lplncvrlvol2  39653  lplncvrlvol  39654  lvolcmp  39655  2lplnm2N  39659  2lplnmj  39660  dalempjsen  39691  dalemcea  39698  dalem2  39699  dalemdea  39700  dalem9  39710  dalem16  39717  dalemcjden  39730  dalem21  39732  dalem23  39734  dalem39  39749  dalem54  39764  dalem60  39770  cdlemb  39832  elpadd2at  39844  paddasslem4  39861  paddasslem7  39864  paddasslem15  39872  paddasslem16  39873  pmodlem1  39884  pmodlem2  39885  llnexchb2  39907  pclfinclN  39988  osumcllem9N  40002  pmapojoinN  40006  pexmidN  40007  pl42lem1N  40017  lhp0lt  40041  lhpexle1  40046  lhpexle2lem  40047  lhpexle3lem  40049  lhprelat3N  40078  ltrnid  40173  trlval3  40225  arglem1N  40228  cdlemc5  40233  cdleme3b  40267  cdleme3c  40268  cdleme3h  40273  cdleme7e  40285  cdleme7ga  40286  cdleme20l1  40358  cdleme20l2  40359  cdleme20l  40360  cdleme22b  40379  cdlemefrs29clN  40437  cdlemefrs32fva  40438  cdlemeg46fvcl  40544  cdlemeg46c  40551  cdlemeg46fvaw  40554  cdlemeg46req  40567  cdleme48fgv  40576  cdlemf1  40599  cdlemg1cex  40626  cdlemg2dN  40628  cdlemg2ce  40630  cdlemg12e  40685  cdlemg35  40751  cdlemh  40855  tendocan  40862  cdlemk28-3  40946  tendoex  41013  dih1  41324  dihmeetlem9N  41353  dihlspsnssN  41370  dihlspsnat  41371  lcfrlem23  41603  renegneg  42444  fsuppind  42622  flt4lem4  42681  3cubes  42722  mzpsubst  42780  rencldnfi  42853  irrapx1  42860  pellexlem3  42863  pellexlem5  42865  infmrgelbi  42910  pellqrex  42911  pellfundge  42914  rmspecfund  42941  congtr  42997  acongeq  43015  jm2.20nn  43029  jm2.25lem1  43030  jm2.26  43034  expdiophlem1  43053  hbtlem2  43156  cantnftermord  43352  suprleubrd  44198  suprlubrd  44200  suprnmpt  45210  wessf1ornlem  45221  mpct  45237  upbdrech  45345  ssfiunibd  45349  uzfissfz  45364  xleadd2d  45365  suprltrp  45366  xleadd1d  45367  suprleubrnmpt  45459  iccintsng  45562  limcrecl  45668  fnlimfvre  45711  dvmulcncf  45962  dvdivcncf  45964  dvbdfbdioolem1  45965  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  stoweidlem1  46038  stoweidlem20  46057  stoweidlem24  46061  stoweidlem34  46071  stoweidlem45  46082  stoweidlem60  46097  fourierdlem20  46164  fourierdlem31  46175  fourierdlem38  46182  fourierdlem64  46207  fourierdlem79  46222  fourierdlem94  46237  fourierdlem113  46256  fouriersw  46268  fouriercn  46269  sge0isum  46464  hoicvr  46585  ovnsubaddlem2  46608  hoidmv1lelem1  46628  hoidmv1lelem3  46630  hoidmvlelem1  46632  hoidmvlelem4  46635  smflimlem2  46809  fmtnof1  47565  lighneallem2  47636  uspgrlim  48022  upgrwlkupwlk  48170  lincresunit3  48512  elbigolo1  48588  eenglngeehlnm  48770