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  1778  3rspcedvdw  3597  elovmpt3rab1  7613  smo11  8294  omeulem2  8508  oeeui  8527  oaabs2  8574  omabs  8576  omxpenlem  9002  map2xp  9071  mapdom2  9072  fsuppsssupp  9290  cantnflt  9587  cnfcom  9615  mapdjuen  10094  pwsdompw  10116  ackbij1lem5  10136  cofsmo  10182  fin1a2lem4  10316  ltmul12a  11998  lt2msq1  12027  ledivp1  12045  lemul1ad  12082  lemul2ad  12083  suprubd  12105  supaddc  12110  supadd  12111  supmul1  12112  supmul  12115  rpnnen1lem3  12898  rpnnen1lem5  12900  lediv2ad  12977  xaddge0  13178  xadddi  13215  xadddi2  13217  supicc  13422  supicclub  13424  difelfznle  13563  flval3  13737  expcan  14094  ltexp2  14095  ltexp2r  14098  expubnd  14103  ltexp2rd  14173  ltexp2d  14176  leexp2d  14177  expcand  14178  hashmap  14360  swrds1  14591  ccatswrd  14593  pfxfv  14607  swrdccatin1  14649  pfxccatin12lem3  14656  cshwidxmod  14727  wrdl3s3  14887  o1fsum  15738  mertenslem1  15809  eftlub  16036  rpnnen2lem4  16144  ruclem12  16168  dvdsadd  16231  3dvds  16260  divalgmod  16335  bitsmod  16365  bitsinv1lem  16370  bezoutlem4  16471  gcdzeq  16481  rplpwr  16487  sqgcd  16491  expgcd  16492  rpmulgcd2  16585  rpdvds  16589  coprmproddvdslem  16591  isprm5  16636  divgcdodd  16639  dvdszzq  16650  divnumden  16677  crth  16707  phimullem  16708  modprm0  16735  modprmn0modprm0  16737  coprimeprodsq2  16739  pythagtriplem19  16763  pockthlem  16835  prmunb  16844  prmreclem3  16848  prmreclem6  16851  ramub  16943  ramz  16955  kerf1ghm  19144  pmtrprfv  19350  pmtrprfv3  19351  mndodcong  19439  odngen  19474  pgpfi  19502  sylow2blem3  19519  lsmless1  19557  lsmless2  19558  lsmless12  19559  lsmmod2  19573  pj1id  19596  odadd2  19746  gexexlem  19749  ablfacrplem  19964  ablfacrp  19965  ablfac1b  19969  ablfac1eu  19972  pgpfac1lem2  19974  ogrpaddlt  20035  elrhmunit  20413  rrgnz  20607  ornglmullt  20772  orngrmullt  20773  lsmssspx  21010  lspsncv0  21071  znunit  21488  uvcvvcl2  21713  uvcvv1  21714  uvcvv0  21715  coe1subfv  22168  coe1fzgsumdlem  22206  scmate  22413  mdetunilem2  22516  pmatcoe1fsupp  22604  mat2pmatlin  22638  decpmatmullem  22674  pmatcollpw1lem1  22677  pmatcollpw1lem2  22678  pm2mpghm  22719  chpscmat  22745  chp0mat  22749  chpidmat  22750  cpmadugsumlemB  22777  cpmadugsumlemC  22778  cpmadugsumlemF  22779  clsndisj  22978  neiptopnei  23035  rnelfm  23856  fmfnfmlem2  23858  fmfnfm  23861  flimss1  23876  isfcf  23937  cnextfun  23967  cnextfvval  23968  cnextf  23969  cnextcn  23970  cnextfres1  23971  ustuqtop1  24145  utopsnneiplem  24151  xblss2ps  24305  xblss2  24306  stdbdxmet  24419  metcnpi3  24450  metustexhalf  24460  nmoi  24632  nmoi2  24634  nmoco  24641  blcvx  24702  icccmplem2  24728  icccmplem3  24729  reconnlem2  24732  xrge0gsumle  24738  metds0  24755  metdstri  24756  metdseq0  24759  lebnumlem3  24878  nmoleub2lem  25030  bcthlem5  25244  csschl  25292  minveclem2  25342  minveclem3b  25344  minveclem4  25348  minveclem6  25350  icombl  25481  cncombf  25575  mbflimsup  25583  itg2monolem1  25667  itg2cnlem1  25678  itg2cnlem2  25679  bddmulibl  25756  ellimc2  25794  cpnord  25853  cpnres  25855  dvmulbr  25857  dvmulbrOLD  25858  dvcobr  25865  dvcobrOLD  25866  dvlipcn  25915  dvlip2  25916  dvivthlem1  25929  lhop1lem  25934  lhop1  25935  dvfsumlem2  25949  dvfsumlem2OLD  25950  itgsubstlem  25971  deg1add  26024  deg1sublt  26031  ply1remlem  26086  plyeq0lem  26131  taylthlem2  26298  taylthlem2OLD  26299  ulmdvlem3  26327  abelthlem7  26364  pilem2  26378  pilem3  26379  pige3ALT  26445  logccv  26588  cxpaddlelem  26677  cvxcl  26911  fsumharmonic  26938  ftalem5  27003  mpodvdsmulf1o  27120  dvdsmulf1o  27122  bposlem1  27211  lgsqr  27278  lgsquad2lem2  27312  2lgsoddprmlem1  27335  2sqlem8a  27352  2sqlem8  27353  dchrmusum2  27421  dchrvmasumiflem1  27428  dchrisum0flblem1  27435  dchrisum0lem1b  27442  pntlem3  27536  noetasuplem4  27664  noetainflem4  27668  noetalem1  27669  divsmulwd  28120  divsclwd  28122  uzsind  28316  tgdim01  28470  axsegcon  28890  ax5seglem1  28891  ax5seglem2  28892  axlowdimlem6  28910  axeuclidlem  28925  axcontlem7  28933  axcontlem9  28935  axcontlem10  28936  nbupgr  29307  nbumgrvtx  29309  cusgrsize2inds  29417  upgriswlk  29604  2pthnloop  29694  numclwwlk2lem1  30338  frgrreg  30356  nmoub3i  30735  ubthlem3  30834  minvecolem2  30837  minvecolem4  30842  minvecolem5  30843  minvecolem6  30844  htthlem  30879  pjpjpre  31381  chscllem1  31599  chscllem2  31600  chscllem3  31601  cnlnadjlem2  32030  leopnmid  32100  tpssad  32501  br8d  32571  swrdf1  32911  splfv3  32913  symgcom2  33039  cyc3genpmlem  33106  archirngz  33141  elrgspnlem1  33192  rlocf1  33223  subrdom  33234  dvdsruasso  33332  unitpidl1  33371  elrspunidl  33375  qsidomlem1  33399  ssdifidlprm  33405  mxidlirredi  33418  1arithidomlem2  33483  1arithidom  33484  1arithufdlem3  33493  ply1gsumz  33540  lssdimle  33579  dimkerim  33599  fedgmullem2  33602  fedgmul  33603  assalactf1o  33607  fldextrspundglemul  33650  fldextrspundgdvds  33652  minplyirred  33677  irredminply  33682  algextdeglem2  33684  rtelextdg2lem  33692  constrext2chnlem  33716  constrresqrtcl  33743  2sqr3minply  33746  cos9thpiminplylem2  33749  cos9thpiminply  33754  qqhval2lem  33947  qqhnm  33956  qqhucn  33958  esumcst  34029  esumpcvgval  34044  measunl  34182  dya2iocbrsiga  34242  dya2icobrsiga  34243  omssubadd  34267  inelcarsg  34278  carsgclctunlem2  34286  sibfof  34307  sitgaddlemb  34315  oddpwdc  34321  eulerpartlemgc  34329  bayesth  34406  ftc2re  34565  breprexplemc  34599  tgoldbachgt  34630  erdszelem8  35170  2goelgoanfmla1  35396  br8  35728  matunitlindflem2  37596  totbndbnd  37768  prdsbnd  37772  rrncmslem  37811  rrntotbnd  37815  isdrngo2  37937  lsatcmp  38981  lcvexchlem2  39013  lcvexchlem3  39014  ncvr1  39250  cvrletrN  39251  cvrnbtwn3  39254  cvrnrefN  39260  cvrcmp  39261  0ltat  39269  atnle0  39287  atlen0  39288  cvlcvr1  39317  cvrval3  39392  atle  39415  athgt  39435  1cvratex  39452  ps-2  39457  ps-2b  39461  llnnleat  39492  2atneat  39494  llnle  39497  atcvrlln  39499  llncmp  39501  2llnmat  39503  2at0mat0  39504  2atm  39506  ps-2c  39507  lplnle  39519  lplnnle2at  39520  llncvrlpln2  39536  llncvrlpln  39537  2lplnmN  39538  2llnmj  39539  2atmat  39540  lplncmp  39541  lplnexllnN  39543  2llnm2N  39547  2llnm4  39549  lvolnle3at  39561  4atlem3a  39576  4atlem3b  39577  4atlem10  39585  4atlem11  39588  4atlem12  39591  lplncvrlvol2  39594  lplncvrlvol  39595  lvolcmp  39596  2lplnm2N  39600  2lplnmj  39601  dalempjsen  39632  dalemcea  39639  dalem2  39640  dalemdea  39641  dalem9  39651  dalem16  39658  dalemcjden  39671  dalem21  39673  dalem23  39675  dalem39  39690  dalem54  39705  dalem60  39711  cdlemb  39773  elpadd2at  39785  paddasslem4  39802  paddasslem7  39805  paddasslem15  39813  paddasslem16  39814  pmodlem1  39825  pmodlem2  39826  llnexchb2  39848  pclfinclN  39929  osumcllem9N  39943  pmapojoinN  39947  pexmidN  39948  pl42lem1N  39958  lhp0lt  39982  lhpexle1  39987  lhpexle2lem  39988  lhpexle3lem  39990  lhprelat3N  40019  ltrnid  40114  trlval3  40166  arglem1N  40169  cdlemc5  40174  cdleme3b  40208  cdleme3c  40209  cdleme3h  40214  cdleme7e  40226  cdleme7ga  40227  cdleme20l1  40299  cdleme20l2  40300  cdleme20l  40301  cdleme22b  40320  cdlemefrs29clN  40378  cdlemefrs32fva  40379  cdlemeg46fvcl  40485  cdlemeg46c  40492  cdlemeg46fvaw  40495  cdlemeg46req  40508  cdleme48fgv  40517  cdlemf1  40540  cdlemg1cex  40567  cdlemg2dN  40569  cdlemg2ce  40571  cdlemg12e  40626  cdlemg35  40692  cdlemh  40796  tendocan  40803  cdlemk28-3  40887  tendoex  40954  dih1  41265  dihmeetlem9N  41294  dihlspsnssN  41311  dihlspsnat  41312  lcfrlem23  41544  renegneg  42385  fsuppind  42563  flt4lem4  42622  3cubes  42663  mzpsubst  42721  rencldnfi  42794  irrapx1  42801  pellexlem3  42804  pellexlem5  42806  infmrgelbi  42851  pellqrex  42852  pellfundge  42855  rmspecfund  42882  congtr  42938  acongeq  42956  jm2.20nn  42970  jm2.25lem1  42971  jm2.26  42975  expdiophlem1  42994  hbtlem2  43097  cantnftermord  43293  suprleubrd  44139  suprlubrd  44141  suprnmpt  45152  wessf1ornlem  45163  mpct  45179  upbdrech  45287  ssfiunibd  45291  uzfissfz  45306  xleadd2d  45307  suprltrp  45308  xleadd1d  45309  suprleubrnmpt  45402  iccintsng  45505  limcrecl  45611  fnlimfvre  45656  dvmulcncf  45907  dvdivcncf  45909  dvbdfbdioolem1  45910  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  stoweidlem1  45983  stoweidlem20  46002  stoweidlem24  46006  stoweidlem34  46016  stoweidlem45  46027  stoweidlem60  46042  fourierdlem20  46109  fourierdlem31  46120  fourierdlem38  46127  fourierdlem64  46152  fourierdlem79  46167  fourierdlem94  46182  fourierdlem113  46201  fouriersw  46213  fouriercn  46214  sge0isum  46409  hoicvr  46530  ovnsubaddlem2  46553  hoidmv1lelem1  46573  hoidmv1lelem3  46575  hoidmvlelem1  46577  hoidmvlelem4  46580  smflimlem2  46754  fmtnof1  47520  lighneallem2  47591  uspgrlim  47977  upgrwlkupwlk  48125  lincresunit3  48467  elbigolo1  48543  eenglngeehlnm  48725