Theorem syl31anc 1376

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl32anc  1381  stoic4b  1780  3rspcedvdw  3582  elovmpt3rab1  7627  smo11  8304  omeulem2  8518  oeeui  8538  oaabs2  8585  omabs  8587  omxpenlem  9016  map2xp  9085  mapdom2  9086  fsuppsssupp  9294  cantnflt  9593  cnfcom  9621  mapdjuen  10103  pwsdompw  10125  ackbij1lem5  10145  cofsmo  10191  fin1a2lem4  10325  ltmul12a  12011  lt2msq1  12040  ledivp1  12058  lemul1ad  12095  lemul2ad  12096  suprubd  12118  supaddc  12123  supadd  12124  supmul1  12125  supmul  12128  rpnnen1lem3  12929  rpnnen1lem5  12931  lediv2ad  13008  xaddge0  13210  xadddi  13247  xadddi2  13249  supicc  13454  supicclub  13456  difelfznle  13596  flval3  13774  expcan  14131  ltexp2  14132  ltexp2r  14135  expubnd  14140  ltexp2rd  14210  ltexp2d  14213  leexp2d  14214  expcand  14215  hashmap  14397  swrds1  14629  ccatswrd  14631  pfxfv  14645  swrdccatin1  14687  pfxccatin12lem3  14694  cshwidxmod  14765  wrdl3s3  14924  o1fsum  15776  mertenslem1  15849  eftlub  16076  rpnnen2lem4  16184  ruclem12  16208  dvdsadd  16271  3dvds  16300  divalgmod  16375  bitsmod  16405  bitsinv1lem  16410  bezoutlem4  16511  gcdzeq  16521  rplpwr  16527  sqgcd  16531  expgcd  16532  rpmulgcd2  16625  rpdvds  16629  coprmproddvdslem  16631  isprm5  16677  divgcdodd  16680  dvdszzq  16691  divnumden  16718  crth  16748  phimullem  16749  modprm0  16776  modprmn0modprm0  16778  coprimeprodsq2  16780  pythagtriplem19  16804  pockthlem  16876  prmunb  16885  prmreclem3  16889  prmreclem6  16892  ramub  16984  ramz  16996  kerf1ghm  19222  pmtrprfv  19428  pmtrprfv3  19429  mndodcong  19517  odngen  19552  pgpfi  19580  sylow2blem3  19597  lsmless1  19635  lsmless2  19636  lsmless12  19637  lsmmod2  19651  pj1id  19674  odadd2  19824  gexexlem  19827  ablfacrplem  20042  ablfacrp  20043  ablfac1b  20047  ablfac1eu  20050  pgpfac1lem2  20052  ogrpaddlt  20113  elrhmunit  20487  rrgnz  20681  ornglmullt  20846  orngrmullt  20847  lsmssspx  21083  lspsncv0  21144  znunit  21543  uvcvvcl2  21768  uvcvv1  21769  uvcvv0  21770  coe1subfv  22231  coe1fzgsumdlem  22268  scmate  22475  mdetunilem2  22578  pmatcoe1fsupp  22666  mat2pmatlin  22700  decpmatmullem  22736  pmatcollpw1lem1  22739  pmatcollpw1lem2  22740  pm2mpghm  22781  chpscmat  22807  chp0mat  22811  chpidmat  22812  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  clsndisj  23040  neiptopnei  23097  rnelfm  23918  fmfnfmlem2  23920  fmfnfm  23923  flimss1  23938  isfcf  23999  cnextfun  24029  cnextfvval  24030  cnextf  24031  cnextcn  24032  cnextfres1  24033  ustuqtop1  24206  utopsnneiplem  24212  xblss2ps  24366  xblss2  24367  stdbdxmet  24480  metcnpi3  24511  metustexhalf  24521  nmoi  24693  nmoi2  24695  nmoco  24702  blcvx  24763  icccmplem2  24789  icccmplem3  24790  reconnlem2  24793  xrge0gsumle  24799  metds0  24816  metdstri  24817  metdseq0  24820  lebnumlem3  24930  nmoleub2lem  25081  bcthlem5  25295  csschl  25343  minveclem2  25393  minveclem3b  25395  minveclem4  25399  minveclem6  25401  icombl  25531  cncombf  25625  mbflimsup  25633  itg2monolem1  25717  itg2cnlem1  25728  itg2cnlem2  25729  bddmulibl  25806  ellimc2  25844  cpnord  25902  cpnres  25904  dvmulbr  25906  dvcobr  25913  dvlipcn  25961  dvlip2  25962  dvivthlem1  25975  lhop1lem  25980  lhop1  25981  dvfsumlem2  25994  itgsubstlem  26015  deg1add  26068  deg1sublt  26075  ply1remlem  26130  plyeq0lem  26175  taylthlem2  26339  ulmdvlem3  26367  abelthlem7  26403  pilem2  26417  pilem3  26418  pige3ALT  26484  logccv  26627  cxpaddlelem  26715  cvxcl  26948  fsumharmonic  26975  ftalem5  27040  mpodvdsmulf1o  27157  dvdsmulf1o  27159  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  divmulswd  28186  divsclwd  28188  uzsind  28397  tgdim01  28575  axsegcon  28996  ax5seglem1  28997  ax5seglem2  28998  axlowdimlem6  29016  axeuclidlem  29031  axcontlem7  29039  axcontlem9  29041  axcontlem10  29042  nbupgr  29413  nbumgrvtx  29415  cusgrsize2inds  29522  upgriswlk  29709  2pthnloop  29799  numclwwlk2lem1  30446  frgrreg  30464  nmoub3i  30844  ubthlem3  30943  minvecolem2  30946  minvecolem4  30951  minvecolem5  30952  minvecolem6  30953  htthlem  30988  pjpjpre  31490  chscllem1  31708  chscllem2  31709  chscllem3  31710  cnlnadjlem2  32139  leopnmid  32209  tpssad  32609  br8d  32681  swrdf1  33016  splfv3  33018  symgcom2  33145  cyc3genpmlem  33212  archirngz  33250  elrgspnlem1  33303  rlocf1  33334  subrdom  33346  dvdsruasso  33445  unitpidl1  33484  elrspunidl  33488  qsidomlem1  33512  ssdifidlprm  33518  mxidlirredi  33531  1arithidomlem2  33596  1arithidom  33597  1arithufdlem3  33606  ply1gsumz  33659  esplymhp  33712  esplyfvaln  33718  vietadeg1  33722  lssdimle  33752  dimkerim  33771  fedgmullem2  33774  fedgmul  33775  assalactf1o  33779  fldextrspundglemul  33823  fldextrspundgdvds  33825  minplyirred  33855  irredminply  33860  algextdeglem2  33862  rtelextdg2lem  33870  constrext2chnlem  33894  constrresqrtcl  33921  2sqr3minply  33924  cos9thpiminplylem2  33927  cos9thpiminply  33932  qqhval2lem  34125  qqhnm  34134  qqhucn  34136  esumcst  34207  esumpcvgval  34222  measunl  34360  dya2iocbrsiga  34419  dya2icobrsiga  34420  omssubadd  34444  inelcarsg  34455  carsgclctunlem2  34463  sibfof  34484  sitgaddlemb  34492  oddpwdc  34498  eulerpartlemgc  34506  bayesth  34583  ftc2re  34742  breprexplemc  34776  tgoldbachgt  34807  erdszelem8  35380  2goelgoanfmla1  35606  br8  35938  matunitlindflem2  37938  totbndbnd  38110  prdsbnd  38114  rrncmslem  38153  rrntotbnd  38157  isdrngo2  38279  lsatcmp  39449  lcvexchlem2  39481  lcvexchlem3  39482  ncvr1  39718  cvrletrN  39719  cvrnbtwn3  39722  cvrnrefN  39728  cvrcmp  39729  0ltat  39737  atnle0  39755  atlen0  39756  cvlcvr1  39785  cvrval3  39859  atle  39882  athgt  39902  1cvratex  39919  ps-2  39924  ps-2b  39928  llnnleat  39959  2atneat  39961  llnle  39964  atcvrlln  39966  llncmp  39968  2llnmat  39970  2at0mat0  39971  2atm  39973  ps-2c  39974  lplnle  39986  lplnnle2at  39987  llncvrlpln2  40003  llncvrlpln  40004  2lplnmN  40005  2llnmj  40006  2atmat  40007  lplncmp  40008  lplnexllnN  40010  2llnm2N  40014  2llnm4  40016  lvolnle3at  40028  4atlem3a  40043  4atlem3b  40044  4atlem10  40052  4atlem11  40055  4atlem12  40058  lplncvrlvol2  40061  lplncvrlvol  40062  lvolcmp  40063  2lplnm2N  40067  2lplnmj  40068  dalempjsen  40099  dalemcea  40106  dalem2  40107  dalemdea  40108  dalem9  40118  dalem16  40125  dalemcjden  40138  dalem21  40140  dalem23  40142  dalem39  40157  dalem54  40172  dalem60  40178  cdlemb  40240  elpadd2at  40252  paddasslem4  40269  paddasslem7  40272  paddasslem15  40280  paddasslem16  40281  pmodlem1  40292  pmodlem2  40293  llnexchb2  40315  pclfinclN  40396  osumcllem9N  40410  pmapojoinN  40414  pexmidN  40415  pl42lem1N  40425  lhp0lt  40449  lhpexle1  40454  lhpexle2lem  40455  lhpexle3lem  40457  lhprelat3N  40486  ltrnid  40581  trlval3  40633  arglem1N  40636  cdlemc5  40641  cdleme3b  40675  cdleme3c  40676  cdleme3h  40681  cdleme7e  40693  cdleme7ga  40694  cdleme20l1  40766  cdleme20l2  40767  cdleme20l  40768  cdleme22b  40787  cdlemefrs29clN  40845  cdlemefrs32fva  40846  cdlemeg46fvcl  40952  cdlemeg46c  40959  cdlemeg46fvaw  40962  cdlemeg46req  40975  cdleme48fgv  40984  cdlemf1  41007  cdlemg1cex  41034  cdlemg2dN  41036  cdlemg2ce  41038  cdlemg12e  41093  cdlemg35  41159  cdlemh  41263  tendocan  41270  cdlemk28-3  41354  tendoex  41421  dih1  41732  dihmeetlem9N  41761  dihlspsnssN  41778  dihlspsnat  41779  lcfrlem23  42011  renegneg  42844  fsuppind  43023  flt4lem4  43082  3cubes  43122  mzpsubst  43180  rencldnfi  43249  irrapx1  43256  pellexlem3  43259  pellexlem5  43261  infmrgelbi  43306  pellqrex  43307  pellfundge  43310  rmspecfund  43337  congtr  43393  acongeq  43411  jm2.20nn  43425  jm2.25lem1  43426  jm2.26  43430  expdiophlem1  43449  hbtlem2  43552  cantnftermord  43748  suprleubrd  44593  suprlubrd  44595  suprnmpt  45604  wessf1ornlem  45615  mpct  45630  upbdrech  45738  ssfiunibd  45742  uzfissfz  45756  xleadd2d  45757  suprltrp  45758  xleadd1d  45759  suprleubrnmpt  45850  iccintsng  45953  limcrecl  46059  fnlimfvre  46102  dvmulcncf  46353  dvdivcncf  46355  dvbdfbdioolem1  46356  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem1  46429  stoweidlem20  46448  stoweidlem24  46452  stoweidlem34  46462  stoweidlem45  46473  stoweidlem60  46488  fourierdlem20  46555  fourierdlem31  46566  fourierdlem38  46573  fourierdlem64  46598  fourierdlem79  46613  fourierdlem94  46628  fourierdlem113  46647  fouriersw  46659  fouriercn  46660  sge0isum  46855  hoicvr  46976  ovnsubaddlem2  46999  hoidmv1lelem1  47019  hoidmv1lelem3  47021  hoidmvlelem1  47023  hoidmvlelem4  47026  smflimlem2  47200  2timesltsq  47826  fmtnof1  47998  lighneallem2  48069  uspgrlim  48468  upgrwlkupwlk  48616  lincresunit3  48957  elbigolo1  49033  eenglngeehlnm  49215