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  3619  elovmpt3rab1  7667  smo11  8378  omeulem2  8595  oeeui  8614  oaabs2  8661  omabs  8663  omxpenlem  9087  map2xp  9161  mapdom2  9162  fsuppsssupp  9393  cantnflt  9686  cnfcom  9714  mapdjuen  10195  pwsdompw  10217  ackbij1lem5  10237  cofsmo  10283  fin1a2lem4  10417  ltmul12a  12097  lt2msq1  12126  ledivp1  12144  lemul1ad  12181  lemul2ad  12182  suprubd  12204  supaddc  12209  supadd  12210  supmul1  12211  supmul  12214  rpnnen1lem3  12995  rpnnen1lem5  12997  lediv2ad  13073  xaddge0  13274  xadddi  13311  xadddi2  13313  supicc  13518  supicclub  13520  difelfznle  13659  flval3  13832  expcan  14187  ltexp2  14188  ltexp2r  14191  expubnd  14196  ltexp2rd  14266  ltexp2d  14269  leexp2d  14270  expcand  14271  hashmap  14453  swrds1  14684  ccatswrd  14686  pfxfv  14700  swrdccatin1  14743  pfxccatin12lem3  14750  cshwidxmod  14821  wrdl3s3  14981  o1fsum  15829  mertenslem1  15900  eftlub  16127  rpnnen2lem4  16235  ruclem12  16259  dvdsadd  16321  3dvds  16350  divalgmod  16425  bitsmod  16455  bitsinv1lem  16460  bezoutlem4  16561  gcdzeq  16571  rplpwr  16577  sqgcd  16581  expgcd  16582  rpmulgcd2  16675  rpdvds  16679  coprmproddvdslem  16681  isprm5  16726  divgcdodd  16729  dvdszzq  16740  divnumden  16767  crth  16797  phimullem  16798  modprm0  16825  modprmn0modprm0  16827  coprimeprodsq2  16829  pythagtriplem19  16853  pockthlem  16925  prmunb  16934  prmreclem3  16938  prmreclem6  16941  ramub  17033  ramz  17045  kerf1ghm  19230  pmtrprfv  19434  pmtrprfv3  19435  mndodcong  19523  odngen  19558  pgpfi  19586  sylow2blem3  19603  lsmless1  19641  lsmless2  19642  lsmless12  19643  lsmmod2  19657  pj1id  19680  odadd2  19830  gexexlem  19833  ablfacrplem  20048  ablfacrp  20049  ablfac1b  20053  ablfac1eu  20056  pgpfac1lem2  20058  elrhmunit  20470  rrgnz  20664  lsmssspx  21046  lspsncv0  21107  znunit  21524  uvcvvcl2  21748  uvcvv1  21749  uvcvv0  21750  coe1subfv  22203  coe1fzgsumdlem  22241  scmate  22448  mdetunilem2  22551  pmatcoe1fsupp  22639  mat2pmatlin  22673  decpmatmullem  22709  pmatcollpw1lem1  22712  pmatcollpw1lem2  22713  pm2mpghm  22754  chpscmat  22780  chp0mat  22784  chpidmat  22785  cpmadugsumlemB  22812  cpmadugsumlemC  22813  cpmadugsumlemF  22814  clsndisj  23013  neiptopnei  23070  rnelfm  23891  fmfnfmlem2  23893  fmfnfm  23896  flimss1  23911  isfcf  23972  cnextfun  24002  cnextfvval  24003  cnextf  24004  cnextcn  24005  cnextfres1  24006  ustuqtop1  24180  utopsnneiplem  24186  xblss2ps  24340  xblss2  24341  stdbdxmet  24454  metcnpi3  24485  metustexhalf  24495  nmoi  24667  nmoi2  24669  nmoco  24676  blcvx  24737  icccmplem2  24763  icccmplem3  24764  reconnlem2  24767  xrge0gsumle  24773  metds0  24790  metdstri  24791  metdseq0  24794  lebnumlem3  24913  nmoleub2lem  25065  bcthlem5  25280  csschl  25328  minveclem2  25378  minveclem3b  25380  minveclem4  25384  minveclem6  25386  icombl  25517  cncombf  25611  mbflimsup  25619  itg2monolem1  25703  itg2cnlem1  25714  itg2cnlem2  25715  bddmulibl  25792  ellimc2  25830  cpnord  25889  cpnres  25891  dvmulbr  25893  dvmulbrOLD  25894  dvcobr  25901  dvcobrOLD  25902  dvlipcn  25951  dvlip2  25952  dvivthlem1  25965  lhop1lem  25970  lhop1  25971  dvfsumlem2  25985  dvfsumlem2OLD  25986  itgsubstlem  26007  deg1add  26060  deg1sublt  26067  ply1remlem  26122  plyeq0lem  26167  taylthlem2  26334  taylthlem2OLD  26335  ulmdvlem3  26363  abelthlem7  26400  pilem2  26414  pilem3  26415  pige3ALT  26481  logccv  26624  cxpaddlelem  26713  cvxcl  26947  fsumharmonic  26974  ftalem5  27039  mpodvdsmulf1o  27156  dvdsmulf1o  27158  bposlem1  27247  lgsqr  27314  lgsquad2lem2  27348  2lgsoddprmlem1  27371  2sqlem8a  27388  2sqlem8  27389  dchrmusum2  27457  dchrvmasumiflem1  27464  dchrisum0flblem1  27471  dchrisum0lem1b  27478  pntlem3  27572  noetasuplem4  27700  noetainflem4  27704  noetalem1  27705  divsmulwd  28149  divsclwd  28151  uzsind  28345  tgdim01  28486  axsegcon  28906  ax5seglem1  28907  ax5seglem2  28908  axlowdimlem6  28926  axeuclidlem  28941  axcontlem7  28949  axcontlem9  28951  axcontlem10  28952  nbupgr  29323  nbumgrvtx  29325  cusgrsize2inds  29433  upgriswlk  29621  2pthnloop  29713  numclwwlk2lem1  30357  frgrreg  30375  nmoub3i  30754  ubthlem3  30853  minvecolem2  30856  minvecolem4  30861  minvecolem5  30862  minvecolem6  30863  htthlem  30898  pjpjpre  31400  chscllem1  31618  chscllem2  31619  chscllem3  31620  cnlnadjlem2  32049  leopnmid  32119  tpssad  32520  br8d  32590  swrdf1  32932  splfv3  32934  ogrpaddlt  33085  symgcom2  33095  cyc3genpmlem  33162  archirngz  33187  elrgspnlem1  33237  rlocf1  33268  subrdom  33279  ornglmullt  33329  orngrmullt  33330  dvdsruasso  33400  unitpidl1  33439  elrspunidl  33443  qsidomlem1  33467  ssdifidlprm  33473  mxidlirredi  33486  1arithidomlem2  33551  1arithidom  33552  1arithufdlem3  33561  ply1gsumz  33608  lssdimle  33647  dimkerim  33667  fedgmullem2  33670  fedgmul  33671  assalactf1o  33675  fldextrspundglemul  33720  fldextrspundgdvds  33722  minplyirred  33745  irredminply  33750  algextdeglem2  33752  rtelextdg2lem  33760  constrext2chnlem  33784  constrresqrtcl  33811  2sqr3minply  33814  cos9thpiminplylem2  33817  cos9thpiminply  33822  qqhval2lem  34012  qqhnm  34021  qqhucn  34023  esumcst  34094  esumpcvgval  34109  measunl  34247  dya2iocbrsiga  34307  dya2icobrsiga  34308  omssubadd  34332  inelcarsg  34343  carsgclctunlem2  34351  sibfof  34372  sitgaddlemb  34380  oddpwdc  34386  eulerpartlemgc  34394  bayesth  34471  ftc2re  34630  breprexplemc  34664  tgoldbachgt  34695  erdszelem8  35220  2goelgoanfmla1  35446  br8  35773  matunitlindflem2  37641  totbndbnd  37813  prdsbnd  37817  rrncmslem  37856  rrntotbnd  37860  isdrngo2  37982  lsatcmp  39021  lcvexchlem2  39053  lcvexchlem3  39054  ncvr1  39290  cvrletrN  39291  cvrnbtwn3  39294  cvrnrefN  39300  cvrcmp  39301  0ltat  39309  atnle0  39327  atlen0  39328  cvlcvr1  39357  cvrval3  39432  atle  39455  athgt  39475  1cvratex  39492  ps-2  39497  ps-2b  39501  llnnleat  39532  2atneat  39534  llnle  39537  atcvrlln  39539  llncmp  39541  2llnmat  39543  2at0mat0  39544  2atm  39546  ps-2c  39547  lplnle  39559  lplnnle2at  39560  llncvrlpln2  39576  llncvrlpln  39577  2lplnmN  39578  2llnmj  39579  2atmat  39580  lplncmp  39581  lplnexllnN  39583  2llnm2N  39587  2llnm4  39589  lvolnle3at  39601  4atlem3a  39616  4atlem3b  39617  4atlem10  39625  4atlem11  39628  4atlem12  39631  lplncvrlvol2  39634  lplncvrlvol  39635  lvolcmp  39636  2lplnm2N  39640  2lplnmj  39641  dalempjsen  39672  dalemcea  39679  dalem2  39680  dalemdea  39681  dalem9  39691  dalem16  39698  dalemcjden  39711  dalem21  39713  dalem23  39715  dalem39  39730  dalem54  39745  dalem60  39751  cdlemb  39813  elpadd2at  39825  paddasslem4  39842  paddasslem7  39845  paddasslem15  39853  paddasslem16  39854  pmodlem1  39865  pmodlem2  39866  llnexchb2  39888  pclfinclN  39969  osumcllem9N  39983  pmapojoinN  39987  pexmidN  39988  pl42lem1N  39998  lhp0lt  40022  lhpexle1  40027  lhpexle2lem  40028  lhpexle3lem  40030  lhprelat3N  40059  ltrnid  40154  trlval3  40206  arglem1N  40209  cdlemc5  40214  cdleme3b  40248  cdleme3c  40249  cdleme3h  40254  cdleme7e  40266  cdleme7ga  40267  cdleme20l1  40339  cdleme20l2  40340  cdleme20l  40341  cdleme22b  40360  cdlemefrs29clN  40418  cdlemefrs32fva  40419  cdlemeg46fvcl  40525  cdlemeg46c  40532  cdlemeg46fvaw  40535  cdlemeg46req  40548  cdleme48fgv  40557  cdlemf1  40580  cdlemg1cex  40607  cdlemg2dN  40609  cdlemg2ce  40611  cdlemg12e  40666  cdlemg35  40732  cdlemh  40836  tendocan  40843  cdlemk28-3  40927  tendoex  40994  dih1  41305  dihmeetlem9N  41334  dihlspsnssN  41351  dihlspsnat  41352  lcfrlem23  41584  renegneg  42454  fsuppind  42613  flt4lem4  42672  3cubes  42713  mzpsubst  42771  rencldnfi  42844  irrapx1  42851  pellexlem3  42854  pellexlem5  42856  infmrgelbi  42901  pellqrex  42902  pellfundge  42905  rmspecfund  42932  congtr  42989  acongeq  43007  jm2.20nn  43021  jm2.25lem1  43022  jm2.26  43026  expdiophlem1  43045  hbtlem2  43148  cantnftermord  43344  suprleubrd  44190  suprlubrd  44192  suprnmpt  45198  wessf1ornlem  45209  mpct  45225  upbdrech  45334  ssfiunibd  45338  uzfissfz  45353  xleadd2d  45354  suprltrp  45355  xleadd1d  45356  suprleubrnmpt  45449  iccintsng  45552  limcrecl  45658  fnlimfvre  45703  dvmulcncf  45954  dvdivcncf  45956  dvbdfbdioolem1  45957  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  stoweidlem1  46030  stoweidlem20  46049  stoweidlem24  46053  stoweidlem34  46063  stoweidlem45  46074  stoweidlem60  46089  fourierdlem20  46156  fourierdlem31  46167  fourierdlem38  46174  fourierdlem64  46199  fourierdlem79  46214  fourierdlem94  46229  fourierdlem113  46248  fouriersw  46260  fouriercn  46261  sge0isum  46456  hoicvr  46577  ovnsubaddlem2  46600  hoidmv1lelem1  46620  hoidmv1lelem3  46622  hoidmvlelem1  46624  hoidmvlelem4  46627  smflimlem2  46801  fmtnof1  47549  lighneallem2  47620  uspgrlim  48004  upgrwlkupwlk  48115  lincresunit3  48457  elbigolo1  48537  eenglngeehlnm  48719