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  3591  elovmpt3rab1  7612  smo11  8290  omeulem2  8504  oeeui  8523  oaabs2  8570  omabs  8572  omxpenlem  8998  map2xp  9067  mapdom2  9068  fsuppsssupp  9272  cantnflt  9569  cnfcom  9597  mapdjuen  10079  pwsdompw  10101  ackbij1lem5  10121  cofsmo  10167  fin1a2lem4  10301  ltmul12a  11984  lt2msq1  12013  ledivp1  12031  lemul1ad  12068  lemul2ad  12069  suprubd  12091  supaddc  12096  supadd  12097  supmul1  12098  supmul  12101  rpnnen1lem3  12879  rpnnen1lem5  12881  lediv2ad  12958  xaddge0  13159  xadddi  13196  xadddi2  13198  supicc  13403  supicclub  13405  difelfznle  13544  flval3  13721  expcan  14078  ltexp2  14079  ltexp2r  14082  expubnd  14087  ltexp2rd  14157  ltexp2d  14160  leexp2d  14161  expcand  14162  hashmap  14344  swrds1  14576  ccatswrd  14578  pfxfv  14592  swrdccatin1  14634  pfxccatin12lem3  14641  cshwidxmod  14712  wrdl3s3  14871  o1fsum  15722  mertenslem1  15793  eftlub  16020  rpnnen2lem4  16128  ruclem12  16152  dvdsadd  16215  3dvds  16244  divalgmod  16319  bitsmod  16349  bitsinv1lem  16354  bezoutlem4  16455  gcdzeq  16465  rplpwr  16471  sqgcd  16475  expgcd  16476  rpmulgcd2  16569  rpdvds  16573  coprmproddvdslem  16575  isprm5  16620  divgcdodd  16623  dvdszzq  16634  divnumden  16661  crth  16691  phimullem  16692  modprm0  16719  modprmn0modprm0  16721  coprimeprodsq2  16723  pythagtriplem19  16747  pockthlem  16819  prmunb  16828  prmreclem3  16832  prmreclem6  16835  ramub  16927  ramz  16939  kerf1ghm  19161  pmtrprfv  19367  pmtrprfv3  19368  mndodcong  19456  odngen  19491  pgpfi  19519  sylow2blem3  19536  lsmless1  19574  lsmless2  19575  lsmless12  19576  lsmmod2  19590  pj1id  19613  odadd2  19763  gexexlem  19766  ablfacrplem  19981  ablfacrp  19982  ablfac1b  19986  ablfac1eu  19989  pgpfac1lem2  19991  ogrpaddlt  20052  elrhmunit  20427  rrgnz  20621  ornglmullt  20786  orngrmullt  20787  lsmssspx  21024  lspsncv0  21085  znunit  21502  uvcvvcl2  21727  uvcvv1  21728  uvcvv0  21729  coe1subfv  22181  coe1fzgsumdlem  22219  scmate  22426  mdetunilem2  22529  pmatcoe1fsupp  22617  mat2pmatlin  22651  decpmatmullem  22687  pmatcollpw1lem1  22690  pmatcollpw1lem2  22691  pm2mpghm  22732  chpscmat  22758  chp0mat  22762  chpidmat  22763  cpmadugsumlemB  22790  cpmadugsumlemC  22791  cpmadugsumlemF  22792  clsndisj  22991  neiptopnei  23048  rnelfm  23869  fmfnfmlem2  23871  fmfnfm  23874  flimss1  23889  isfcf  23950  cnextfun  23980  cnextfvval  23981  cnextf  23982  cnextcn  23983  cnextfres1  23984  ustuqtop1  24157  utopsnneiplem  24163  xblss2ps  24317  xblss2  24318  stdbdxmet  24431  metcnpi3  24462  metustexhalf  24472  nmoi  24644  nmoi2  24646  nmoco  24653  blcvx  24714  icccmplem2  24740  icccmplem3  24741  reconnlem2  24744  xrge0gsumle  24750  metds0  24767  metdstri  24768  metdseq0  24771  lebnumlem3  24890  nmoleub2lem  25042  bcthlem5  25256  csschl  25304  minveclem2  25354  minveclem3b  25356  minveclem4  25360  minveclem6  25362  icombl  25493  cncombf  25587  mbflimsup  25595  itg2monolem1  25679  itg2cnlem1  25690  itg2cnlem2  25691  bddmulibl  25768  ellimc2  25806  cpnord  25865  cpnres  25867  dvmulbr  25869  dvmulbrOLD  25870  dvcobr  25877  dvcobrOLD  25878  dvlipcn  25927  dvlip2  25928  dvivthlem1  25941  lhop1lem  25946  lhop1  25947  dvfsumlem2  25961  dvfsumlem2OLD  25962  itgsubstlem  25983  deg1add  26036  deg1sublt  26043  ply1remlem  26098  plyeq0lem  26143  taylthlem2  26310  taylthlem2OLD  26311  ulmdvlem3  26339  abelthlem7  26376  pilem2  26390  pilem3  26391  pige3ALT  26457  logccv  26600  cxpaddlelem  26689  cvxcl  26923  fsumharmonic  26950  ftalem5  27015  mpodvdsmulf1o  27132  dvdsmulf1o  27134  bposlem1  27223  lgsqr  27290  lgsquad2lem2  27324  2lgsoddprmlem1  27347  2sqlem8a  27364  2sqlem8  27365  dchrmusum2  27433  dchrvmasumiflem1  27440  dchrisum0flblem1  27447  dchrisum0lem1b  27454  pntlem3  27548  noetasuplem4  27676  noetainflem4  27680  noetalem1  27681  divsmulwd  28134  divsclwd  28136  uzsind  28330  tgdim01  28486  axsegcon  28907  ax5seglem1  28908  ax5seglem2  28909  axlowdimlem6  28927  axeuclidlem  28942  axcontlem7  28950  axcontlem9  28952  axcontlem10  28953  nbupgr  29324  nbumgrvtx  29326  cusgrsize2inds  29434  upgriswlk  29621  2pthnloop  29711  numclwwlk2lem1  30358  frgrreg  30376  nmoub3i  30755  ubthlem3  30854  minvecolem2  30857  minvecolem4  30862  minvecolem5  30863  minvecolem6  30864  htthlem  30899  pjpjpre  31401  chscllem1  31619  chscllem2  31620  chscllem3  31621  cnlnadjlem2  32050  leopnmid  32120  tpssad  32521  br8d  32593  swrdf1  32944  splfv3  32946  symgcom2  33060  cyc3genpmlem  33127  archirngz  33165  elrgspnlem1  33216  rlocf1  33247  subrdom  33258  dvdsruasso  33357  unitpidl1  33396  elrspunidl  33400  qsidomlem1  33424  ssdifidlprm  33430  mxidlirredi  33443  1arithidomlem2  33508  1arithidom  33509  1arithufdlem3  33518  ply1gsumz  33566  esplymhp  33608  lssdimle  33641  dimkerim  33661  fedgmullem2  33664  fedgmul  33665  assalactf1o  33669  fldextrspundglemul  33713  fldextrspundgdvds  33715  minplyirred  33745  irredminply  33750  algextdeglem2  33752  rtelextdg2lem  33760  constrext2chnlem  33784  constrresqrtcl  33811  2sqr3minply  33814  cos9thpiminplylem2  33817  cos9thpiminply  33822  qqhval2lem  34015  qqhnm  34024  qqhucn  34026  esumcst  34097  esumpcvgval  34112  measunl  34250  dya2iocbrsiga  34309  dya2icobrsiga  34310  omssubadd  34334  inelcarsg  34345  carsgclctunlem2  34353  sibfof  34374  sitgaddlemb  34382  oddpwdc  34388  eulerpartlemgc  34396  bayesth  34473  ftc2re  34632  breprexplemc  34666  tgoldbachgt  34697  erdszelem8  35263  2goelgoanfmla1  35489  br8  35821  matunitlindflem2  37677  totbndbnd  37849  prdsbnd  37853  rrncmslem  37892  rrntotbnd  37896  isdrngo2  38018  lsatcmp  39122  lcvexchlem2  39154  lcvexchlem3  39155  ncvr1  39391  cvrletrN  39392  cvrnbtwn3  39395  cvrnrefN  39401  cvrcmp  39402  0ltat  39410  atnle0  39428  atlen0  39429  cvlcvr1  39458  cvrval3  39532  atle  39555  athgt  39575  1cvratex  39592  ps-2  39597  ps-2b  39601  llnnleat  39632  2atneat  39634  llnle  39637  atcvrlln  39639  llncmp  39641  2llnmat  39643  2at0mat0  39644  2atm  39646  ps-2c  39647  lplnle  39659  lplnnle2at  39660  llncvrlpln2  39676  llncvrlpln  39677  2lplnmN  39678  2llnmj  39679  2atmat  39680  lplncmp  39681  lplnexllnN  39683  2llnm2N  39687  2llnm4  39689  lvolnle3at  39701  4atlem3a  39716  4atlem3b  39717  4atlem10  39725  4atlem11  39728  4atlem12  39731  lplncvrlvol2  39734  lplncvrlvol  39735  lvolcmp  39736  2lplnm2N  39740  2lplnmj  39741  dalempjsen  39772  dalemcea  39779  dalem2  39780  dalemdea  39781  dalem9  39791  dalem16  39798  dalemcjden  39811  dalem21  39813  dalem23  39815  dalem39  39830  dalem54  39845  dalem60  39851  cdlemb  39913  elpadd2at  39925  paddasslem4  39942  paddasslem7  39945  paddasslem15  39953  paddasslem16  39954  pmodlem1  39965  pmodlem2  39966  llnexchb2  39988  pclfinclN  40069  osumcllem9N  40083  pmapojoinN  40087  pexmidN  40088  pl42lem1N  40098  lhp0lt  40122  lhpexle1  40127  lhpexle2lem  40128  lhpexle3lem  40130  lhprelat3N  40159  ltrnid  40254  trlval3  40306  arglem1N  40309  cdlemc5  40314  cdleme3b  40348  cdleme3c  40349  cdleme3h  40354  cdleme7e  40366  cdleme7ga  40367  cdleme20l1  40439  cdleme20l2  40440  cdleme20l  40441  cdleme22b  40460  cdlemefrs29clN  40518  cdlemefrs32fva  40519  cdlemeg46fvcl  40625  cdlemeg46c  40632  cdlemeg46fvaw  40635  cdlemeg46req  40648  cdleme48fgv  40657  cdlemf1  40680  cdlemg1cex  40707  cdlemg2dN  40709  cdlemg2ce  40711  cdlemg12e  40766  cdlemg35  40832  cdlemh  40936  tendocan  40943  cdlemk28-3  41027  tendoex  41094  dih1  41405  dihmeetlem9N  41434  dihlspsnssN  41451  dihlspsnat  41452  lcfrlem23  41684  renegneg  42530  fsuppind  42708  flt4lem4  42767  3cubes  42807  mzpsubst  42865  rencldnfi  42938  irrapx1  42945  pellexlem3  42948  pellexlem5  42950  infmrgelbi  42995  pellqrex  42996  pellfundge  42999  rmspecfund  43026  congtr  43082  acongeq  43100  jm2.20nn  43114  jm2.25lem1  43115  jm2.26  43119  expdiophlem1  43138  hbtlem2  43241  cantnftermord  43437  suprleubrd  44283  suprlubrd  44285  suprnmpt  45295  wessf1ornlem  45306  mpct  45322  upbdrech  45430  ssfiunibd  45434  uzfissfz  45449  xleadd2d  45450  suprltrp  45451  xleadd1d  45452  suprleubrnmpt  45544  iccintsng  45647  limcrecl  45753  fnlimfvre  45796  dvmulcncf  46047  dvdivcncf  46049  dvbdfbdioolem1  46050  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  stoweidlem1  46123  stoweidlem20  46142  stoweidlem24  46146  stoweidlem34  46156  stoweidlem45  46167  stoweidlem60  46182  fourierdlem20  46249  fourierdlem31  46260  fourierdlem38  46267  fourierdlem64  46292  fourierdlem79  46307  fourierdlem94  46322  fourierdlem113  46341  fouriersw  46353  fouriercn  46354  sge0isum  46549  hoicvr  46670  ovnsubaddlem2  46693  hoidmv1lelem1  46713  hoidmv1lelem3  46715  hoidmvlelem1  46717  hoidmvlelem4  46720  smflimlem2  46894  fmtnof1  47659  lighneallem2  47730  uspgrlim  48116  upgrwlkupwlk  48264  lincresunit3  48606  elbigolo1  48682  eenglngeehlnm  48864