Theorem syl31anc 1373

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 585	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  syl32anc  1378  stoic4b  1778  elovmpt3rab1  7561  smo11  8226  omeulem2  8445  oeeui  8464  oaabs2  8510  omabs  8512  omxpenlem  8898  map2xp  8972  mapdom2  8973  fsuppsssupp  9188  cantnflt  9474  cnfcom  9502  mapdjuen  9982  pwsdompw  10006  ackbij1lem5  10026  cofsmo  10071  fin1a2lem4  10205  ltmul12a  11877  lt2msq1  11905  ledivp1  11923  lemul1ad  11960  lemul2ad  11961  suprubd  11983  supaddc  11988  supadd  11989  supmul1  11990  supmul  11993  rpnnen1lem3  12765  rpnnen1lem5  12767  lediv2ad  12840  xaddge0  13038  xadddi  13075  xadddi2  13077  supicc  13279  supicclub  13281  difelfznle  13416  flval3  13581  expcan  13933  ltexp2  13934  ltexp2r  13937  expubnd  13941  ltexp2rd  14009  ltexp2d  14014  leexp2d  14015  expcand  14016  hashmap  14195  swrds1  14424  ccatswrd  14426  pfxfv  14440  swrdccatin1  14483  pfxccatin12lem3  14490  cshwidxmod  14561  wrdl3s3  14722  o1fsum  15570  mertenslem1  15641  eftlub  15863  rpnnen2lem4  15971  ruclem12  15995  dvdsadd  16056  3dvds  16085  divalgmod  16160  bitsmod  16188  bitsinv1lem  16193  bezoutlem4  16295  gcdzeq  16307  rplpwr  16312  sqgcd  16315  rpmulgcd2  16406  rpdvds  16410  coprmproddvdslem  16412  isprm5  16457  divgcdodd  16460  divnumden  16497  crth  16524  phimullem  16525  modprm0  16551  modprmn0modprm0  16553  coprimeprodsq2  16555  pythagtriplem19  16579  pockthlem  16651  prmunb  16660  prmreclem3  16664  prmreclem6  16667  ramub  16759  ramz  16771  pmtrprfv  19106  pmtrprfv3  19107  mndodcong  19195  odngen  19227  pgpfi  19255  sylow2blem3  19272  lsmless1  19310  lsmless2  19311  lsmless12  19312  lsmmod2  19327  pj1id  19350  odadd2  19495  gexexlem  19498  ablfacrplem  19713  ablfacrp  19714  ablfac1b  19718  ablfac1eu  19721  pgpfac1lem2  19723  kerf1ghm  20032  lsmssspx  20395  lspsncv0  20453  znunit  20816  uvcvvcl2  21040  uvcvv1  21041  uvcvv0  21042  coe1subfv  21482  coe1fzgsumdlem  21517  scmate  21704  mdetunilem2  21807  pmatcoe1fsupp  21895  mat2pmatlin  21929  decpmatmullem  21965  pmatcollpw1lem1  21968  pmatcollpw1lem2  21969  pm2mpghm  22010  chpscmat  22036  chp0mat  22040  chpidmat  22041  cpmadugsumlemB  22068  cpmadugsumlemC  22069  cpmadugsumlemF  22070  clsndisj  22271  neiptopnei  22328  rnelfm  23149  fmfnfmlem2  23151  fmfnfm  23154  flimss1  23169  isfcf  23230  cnextfun  23260  cnextfvval  23261  cnextf  23262  cnextcn  23263  cnextfres1  23264  ustuqtop1  23438  utopsnneiplem  23444  xblss2ps  23599  xblss2  23600  stdbdxmet  23716  metcnpi3  23747  metustexhalf  23757  nmoi  23937  nmoi2  23939  nmoco  23946  blcvx  24006  icccmplem2  24031  icccmplem3  24032  reconnlem2  24035  xrge0gsumle  24041  metds0  24058  metdstri  24059  metdseq0  24062  lebnumlem3  24171  nmoleub2lem  24322  bcthlem5  24537  csschl  24585  minveclem2  24635  minveclem3b  24637  minveclem4  24641  minveclem6  24643  icombl  24773  cncombf  24867  mbflimsup  24875  itg2monolem1  24960  itg2cnlem1  24971  itg2cnlem2  24972  bddmulibl  25048  ellimc2  25086  cpnord  25144  cpnres  25146  dvmulbr  25148  dvcobr  25155  dvlipcn  25203  dvlip2  25204  dvivthlem1  25217  lhop1lem  25222  lhop1  25223  dvfsumlem2  25236  itgsubstlem  25257  deg1add  25313  deg1sublt  25320  ply1remlem  25372  plyeq0lem  25416  taylthlem2  25578  ulmdvlem3  25606  abelthlem7  25642  pilem2  25656  pilem3  25657  pige3ALT  25721  logccv  25863  cxpaddlelem  25949  cvxcl  26179  fsumharmonic  26206  ftalem5  26271  dvdsmulf1o  26388  bposlem1  26477  lgsqr  26544  lgsquad2lem2  26578  2lgsoddprmlem1  26601  2sqlem8a  26618  2sqlem8  26619  dchrmusum2  26687  dchrvmasumiflem1  26694  dchrisum0flblem1  26701  dchrisum0lem1b  26708  pntlem3  26802  tgdim01  26913  axsegcon  27340  ax5seglem1  27341  ax5seglem2  27342  axlowdimlem6  27360  axeuclidlem  27375  axcontlem7  27383  axcontlem9  27385  axcontlem10  27386  nbupgr  27756  nbumgrvtx  27758  cusgrsize2inds  27865  upgriswlk  28053  2pthnloop  28144  numclwwlk2lem1  28785  frgrreg  28803  nmoub3i  29180  ubthlem3  29279  minvecolem2  29282  minvecolem4  29287  minvecolem5  29288  minvecolem6  29289  htthlem  29324  pjpjpre  29826  chscllem1  30044  chscllem2  30045  chscllem3  30046  cnlnadjlem2  30475  leopnmid  30545  br8d  30995  dvdszzq  31174  swrdf1  31273  splfv3  31275  ogrpaddlt  31388  symgcom2  31398  cyc3genpmlem  31463  archirngz  31488  ornglmullt  31551  orngrmullt  31552  elrhmunit  31564  elrspunidl  31651  qsidomlem1  31673  lssdimle  31736  dimkerim  31753  fedgmullem2  31756  fedgmul  31757  qqhval2lem  31976  qqhnm  31985  qqhucn  31987  esumcst  32076  esumpcvgval  32091  measunl  32229  dya2iocbrsiga  32287  dya2icobrsiga  32288  omssubadd  32312  inelcarsg  32323  carsgclctunlem2  32331  sibfof  32352  sitgaddlemb  32360  oddpwdc  32366  eulerpartlemgc  32374  bayesth  32451  ftc2re  32623  breprexplemc  32657  tgoldbachgt  32688  erdszelem8  33205  2goelgoanfmla1  33431  br8  33768  noetasuplem4  33984  noetainflem4  33988  noetalem1  33989  matunitlindflem2  35818  totbndbnd  35991  prdsbnd  35995  rrncmslem  36034  rrntotbnd  36038  isdrngo2  36160  lsatcmp  37059  lcvexchlem2  37091  lcvexchlem3  37092  ncvr1  37328  cvrletrN  37329  cvrnbtwn3  37332  cvrnrefN  37338  cvrcmp  37339  0ltat  37347  atnle0  37365  atlen0  37366  cvlcvr1  37395  cvrval3  37469  atle  37492  athgt  37512  1cvratex  37529  ps-2  37534  ps-2b  37538  llnnleat  37569  2atneat  37571  llnle  37574  atcvrlln  37576  llncmp  37578  2llnmat  37580  2at0mat0  37581  2atm  37583  ps-2c  37584  lplnle  37596  lplnnle2at  37597  llncvrlpln2  37613  llncvrlpln  37614  2lplnmN  37615  2llnmj  37616  2atmat  37617  lplncmp  37618  lplnexllnN  37620  2llnm2N  37624  2llnm4  37626  lvolnle3at  37638  4atlem3a  37653  4atlem3b  37654  4atlem10  37662  4atlem11  37665  4atlem12  37668  lplncvrlvol2  37671  lplncvrlvol  37672  lvolcmp  37673  2lplnm2N  37677  2lplnmj  37678  dalempjsen  37709  dalemcea  37716  dalem2  37717  dalemdea  37718  dalem9  37728  dalem16  37735  dalemcjden  37748  dalem21  37750  dalem23  37752  dalem39  37767  dalem54  37782  dalem60  37788  cdlemb  37850  elpadd2at  37862  paddasslem4  37879  paddasslem7  37882  paddasslem15  37890  paddasslem16  37891  pmodlem1  37902  pmodlem2  37903  llnexchb2  37925  pclfinclN  38006  osumcllem9N  38020  pmapojoinN  38024  pexmidN  38025  pl42lem1N  38035  lhp0lt  38059  lhpexle1  38064  lhpexle2lem  38065  lhpexle3lem  38067  lhprelat3N  38096  ltrnid  38191  trlval3  38243  arglem1N  38246  cdlemc5  38251  cdleme3b  38285  cdleme3c  38286  cdleme3h  38291  cdleme7e  38303  cdleme7ga  38304  cdleme20l1  38376  cdleme20l2  38377  cdleme20l  38378  cdleme22b  38397  cdlemefrs29clN  38455  cdlemefrs32fva  38456  cdlemeg46fvcl  38562  cdlemeg46c  38569  cdlemeg46fvaw  38572  cdlemeg46req  38585  cdleme48fgv  38594  cdlemf1  38617  cdlemg1cex  38644  cdlemg2dN  38646  cdlemg2ce  38648  cdlemg12e  38703  cdlemg35  38769  cdlemh  38873  tendocan  38880  cdlemk28-3  38964  tendoex  39031  dih1  39342  dihmeetlem9N  39371  dihlspsnssN  39388  dihlspsnat  39389  lcfrlem23  39621  3rspcedvdw  40223  fsuppind  40316  expgcd  40371  renegneg  40431  flt4lem4  40523  3cubes  40549  mzpsubst  40607  rencldnfi  40680  irrapx1  40687  pellexlem3  40690  pellexlem5  40692  infmrgelbi  40737  pellqrex  40738  pellfundge  40741  rmspecfund  40768  congtr  40825  acongeq  40843  jm2.20nn  40857  jm2.25lem1  40858  jm2.26  40862  expdiophlem1  40881  hbtlem2  40987  suprleubrd  41815  suprlubrd  41817  suprnmpt  42754  wessf1ornlem  42766  mpct  42785  upbdrech  42892  ssfiunibd  42896  uzfissfz  42913  xleadd2d  42914  suprltrp  42915  xleadd1d  42916  suprleubrnmpt  43010  iccintsng  43110  limcrecl  43219  fnlimfvre  43264  dvmulcncf  43515  dvdivcncf  43517  dvbdfbdioolem1  43518  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  stoweidlem1  43591  stoweidlem20  43610  stoweidlem24  43614  stoweidlem34  43624  stoweidlem45  43635  stoweidlem60  43650  fourierdlem20  43717  fourierdlem31  43728  fourierdlem38  43735  fourierdlem64  43760  fourierdlem79  43775  fourierdlem94  43790  fourierdlem113  43809  fouriersw  43821  fouriercn  43822  sge0isum  44015  hoicvr  44136  ovnsubaddlem2  44159  hoidmv1lelem1  44179  hoidmv1lelem3  44181  hoidmvlelem1  44183  hoidmvlelem4  44186  smflimlem2  44360  fmtnof1  45045  lighneallem2  45116  upgrwlkupwlk  45360  lincresunit3  45880  elbigolo1  45961  eenglngeehlnm  46143