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  3583  elovmpt3rab1  7620  smo11  8297  omeulem2  8511  oeeui  8531  oaabs2  8578  omabs  8580  omxpenlem  9009  map2xp  9078  mapdom2  9079  fsuppsssupp  9287  cantnflt  9584  cnfcom  9612  mapdjuen  10094  pwsdompw  10116  ackbij1lem5  10136  cofsmo  10182  fin1a2lem4  10316  ltmul12a  12002  lt2msq1  12031  ledivp1  12049  lemul1ad  12086  lemul2ad  12087  suprubd  12109  supaddc  12114  supadd  12115  supmul1  12116  supmul  12119  rpnnen1lem3  12920  rpnnen1lem5  12922  lediv2ad  12999  xaddge0  13201  xadddi  13238  xadddi2  13240  supicc  13445  supicclub  13447  difelfznle  13587  flval3  13765  expcan  14122  ltexp2  14123  ltexp2r  14126  expubnd  14131  ltexp2rd  14201  ltexp2d  14204  leexp2d  14205  expcand  14206  hashmap  14388  swrds1  14620  ccatswrd  14622  pfxfv  14636  swrdccatin1  14678  pfxccatin12lem3  14685  cshwidxmod  14756  wrdl3s3  14915  o1fsum  15767  mertenslem1  15840  eftlub  16067  rpnnen2lem4  16175  ruclem12  16199  dvdsadd  16262  3dvds  16291  divalgmod  16366  bitsmod  16396  bitsinv1lem  16401  bezoutlem4  16502  gcdzeq  16512  rplpwr  16518  sqgcd  16522  expgcd  16523  rpmulgcd2  16616  rpdvds  16620  coprmproddvdslem  16622  isprm5  16668  divgcdodd  16671  dvdszzq  16682  divnumden  16709  crth  16739  phimullem  16740  modprm0  16767  modprmn0modprm0  16769  coprimeprodsq2  16771  pythagtriplem19  16795  pockthlem  16867  prmunb  16876  prmreclem3  16880  prmreclem6  16883  ramub  16975  ramz  16987  kerf1ghm  19213  pmtrprfv  19419  pmtrprfv3  19420  mndodcong  19508  odngen  19543  pgpfi  19571  sylow2blem3  19588  lsmless1  19626  lsmless2  19627  lsmless12  19628  lsmmod2  19642  pj1id  19665  odadd2  19815  gexexlem  19818  ablfacrplem  20033  ablfacrp  20034  ablfac1b  20038  ablfac1eu  20041  pgpfac1lem2  20043  ogrpaddlt  20104  elrhmunit  20478  rrgnz  20672  ornglmullt  20837  orngrmullt  20838  lsmssspx  21075  lspsncv0  21136  znunit  21553  uvcvvcl2  21778  uvcvv1  21779  uvcvv0  21780  coe1subfv  22241  coe1fzgsumdlem  22278  scmate  22485  mdetunilem2  22588  pmatcoe1fsupp  22676  mat2pmatlin  22710  decpmatmullem  22746  pmatcollpw1lem1  22749  pmatcollpw1lem2  22750  pm2mpghm  22791  chpscmat  22817  chp0mat  22821  chpidmat  22822  cpmadugsumlemB  22849  cpmadugsumlemC  22850  cpmadugsumlemF  22851  clsndisj  23050  neiptopnei  23107  rnelfm  23928  fmfnfmlem2  23930  fmfnfm  23933  flimss1  23948  isfcf  24009  cnextfun  24039  cnextfvval  24040  cnextf  24041  cnextcn  24042  cnextfres1  24043  ustuqtop1  24216  utopsnneiplem  24222  xblss2ps  24376  xblss2  24377  stdbdxmet  24490  metcnpi3  24521  metustexhalf  24531  nmoi  24703  nmoi2  24705  nmoco  24712  blcvx  24773  icccmplem2  24799  icccmplem3  24800  reconnlem2  24803  xrge0gsumle  24809  metds0  24826  metdstri  24827  metdseq0  24830  lebnumlem3  24940  nmoleub2lem  25091  bcthlem5  25305  csschl  25353  minveclem2  25403  minveclem3b  25405  minveclem4  25409  minveclem6  25411  icombl  25541  cncombf  25635  mbflimsup  25643  itg2monolem1  25727  itg2cnlem1  25738  itg2cnlem2  25739  bddmulibl  25816  ellimc2  25854  cpnord  25912  cpnres  25914  dvmulbr  25916  dvcobr  25923  dvlipcn  25971  dvlip2  25972  dvivthlem1  25985  lhop1lem  25990  lhop1  25991  dvfsumlem2  26004  itgsubstlem  26025  deg1add  26078  deg1sublt  26085  ply1remlem  26140  plyeq0lem  26185  taylthlem2  26351  taylthlem2OLD  26352  ulmdvlem3  26380  abelthlem7  26416  pilem2  26430  pilem3  26431  pige3ALT  26497  logccv  26640  cxpaddlelem  26728  cvxcl  26962  fsumharmonic  26989  ftalem5  27054  mpodvdsmulf1o  27171  dvdsmulf1o  27173  bposlem1  27261  lgsqr  27328  lgsquad2lem2  27362  2lgsoddprmlem1  27385  2sqlem8a  27402  2sqlem8  27403  dchrmusum2  27471  dchrvmasumiflem1  27478  dchrisum0flblem1  27485  dchrisum0lem1b  27492  pntlem3  27586  noetasuplem4  27714  noetainflem4  27718  noetalem1  27719  divmulswd  28200  divsclwd  28202  uzsind  28411  tgdim01  28589  axsegcon  29010  ax5seglem1  29011  ax5seglem2  29012  axlowdimlem6  29030  axeuclidlem  29045  axcontlem7  29053  axcontlem9  29055  axcontlem10  29056  nbupgr  29427  nbumgrvtx  29429  cusgrsize2inds  29537  upgriswlk  29724  2pthnloop  29814  numclwwlk2lem1  30461  frgrreg  30479  nmoub3i  30859  ubthlem3  30958  minvecolem2  30961  minvecolem4  30966  minvecolem5  30967  minvecolem6  30968  htthlem  31003  pjpjpre  31505  chscllem1  31723  chscllem2  31724  chscllem3  31725  cnlnadjlem2  32154  leopnmid  32224  tpssad  32624  br8d  32696  swrdf1  33031  splfv3  33033  symgcom2  33160  cyc3genpmlem  33227  archirngz  33265  elrgspnlem1  33318  rlocf1  33349  subrdom  33361  dvdsruasso  33460  unitpidl1  33499  elrspunidl  33503  qsidomlem1  33527  ssdifidlprm  33533  mxidlirredi  33546  1arithidomlem2  33611  1arithidom  33612  1arithufdlem3  33621  ply1gsumz  33674  esplymhp  33727  esplyfvaln  33733  vietadeg1  33737  lssdimle  33767  dimkerim  33787  fedgmullem2  33790  fedgmul  33791  assalactf1o  33795  fldextrspundglemul  33839  fldextrspundgdvds  33841  minplyirred  33871  irredminply  33876  algextdeglem2  33878  rtelextdg2lem  33886  constrext2chnlem  33910  constrresqrtcl  33937  2sqr3minply  33940  cos9thpiminplylem2  33943  cos9thpiminply  33948  qqhval2lem  34141  qqhnm  34150  qqhucn  34152  esumcst  34223  esumpcvgval  34238  measunl  34376  dya2iocbrsiga  34435  dya2icobrsiga  34436  omssubadd  34460  inelcarsg  34471  carsgclctunlem2  34479  sibfof  34500  sitgaddlemb  34508  oddpwdc  34514  eulerpartlemgc  34522  bayesth  34599  ftc2re  34758  breprexplemc  34792  tgoldbachgt  34823  erdszelem8  35396  2goelgoanfmla1  35622  br8  35954  matunitlindflem2  37952  totbndbnd  38124  prdsbnd  38128  rrncmslem  38167  rrntotbnd  38171  isdrngo2  38293  lsatcmp  39463  lcvexchlem2  39495  lcvexchlem3  39496  ncvr1  39732  cvrletrN  39733  cvrnbtwn3  39736  cvrnrefN  39742  cvrcmp  39743  0ltat  39751  atnle0  39769  atlen0  39770  cvlcvr1  39799  cvrval3  39873  atle  39896  athgt  39916  1cvratex  39933  ps-2  39938  ps-2b  39942  llnnleat  39973  2atneat  39975  llnle  39978  atcvrlln  39980  llncmp  39982  2llnmat  39984  2at0mat0  39985  2atm  39987  ps-2c  39988  lplnle  40000  lplnnle2at  40001  llncvrlpln2  40017  llncvrlpln  40018  2lplnmN  40019  2llnmj  40020  2atmat  40021  lplncmp  40022  lplnexllnN  40024  2llnm2N  40028  2llnm4  40030  lvolnle3at  40042  4atlem3a  40057  4atlem3b  40058  4atlem10  40066  4atlem11  40069  4atlem12  40072  lplncvrlvol2  40075  lplncvrlvol  40076  lvolcmp  40077  2lplnm2N  40081  2lplnmj  40082  dalempjsen  40113  dalemcea  40120  dalem2  40121  dalemdea  40122  dalem9  40132  dalem16  40139  dalemcjden  40152  dalem21  40154  dalem23  40156  dalem39  40171  dalem54  40186  dalem60  40192  cdlemb  40254  elpadd2at  40266  paddasslem4  40283  paddasslem7  40286  paddasslem15  40294  paddasslem16  40295  pmodlem1  40306  pmodlem2  40307  llnexchb2  40329  pclfinclN  40410  osumcllem9N  40424  pmapojoinN  40428  pexmidN  40429  pl42lem1N  40439  lhp0lt  40463  lhpexle1  40468  lhpexle2lem  40469  lhpexle3lem  40471  lhprelat3N  40500  ltrnid  40595  trlval3  40647  arglem1N  40650  cdlemc5  40655  cdleme3b  40689  cdleme3c  40690  cdleme3h  40695  cdleme7e  40707  cdleme7ga  40708  cdleme20l1  40780  cdleme20l2  40781  cdleme20l  40782  cdleme22b  40801  cdlemefrs29clN  40859  cdlemefrs32fva  40860  cdlemeg46fvcl  40966  cdlemeg46c  40973  cdlemeg46fvaw  40976  cdlemeg46req  40989  cdleme48fgv  40998  cdlemf1  41021  cdlemg1cex  41048  cdlemg2dN  41050  cdlemg2ce  41052  cdlemg12e  41107  cdlemg35  41173  cdlemh  41277  tendocan  41284  cdlemk28-3  41368  tendoex  41435  dih1  41746  dihmeetlem9N  41775  dihlspsnssN  41792  dihlspsnat  41793  lcfrlem23  42025  renegneg  42858  fsuppind  43037  flt4lem4  43096  3cubes  43136  mzpsubst  43194  rencldnfi  43267  irrapx1  43274  pellexlem3  43277  pellexlem5  43279  infmrgelbi  43324  pellqrex  43325  pellfundge  43328  rmspecfund  43355  congtr  43411  acongeq  43429  jm2.20nn  43443  jm2.25lem1  43444  jm2.26  43448  expdiophlem1  43467  hbtlem2  43570  cantnftermord  43766  suprleubrd  44611  suprlubrd  44613  suprnmpt  45622  wessf1ornlem  45633  mpct  45648  upbdrech  45756  ssfiunibd  45760  uzfissfz  45774  xleadd2d  45775  suprltrp  45776  xleadd1d  45777  suprleubrnmpt  45868  iccintsng  45971  limcrecl  46077  fnlimfvre  46120  dvmulcncf  46371  dvdivcncf  46373  dvbdfbdioolem1  46374  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  stoweidlem1  46447  stoweidlem20  46466  stoweidlem24  46470  stoweidlem34  46480  stoweidlem45  46491  stoweidlem60  46506  fourierdlem20  46573  fourierdlem31  46584  fourierdlem38  46591  fourierdlem64  46616  fourierdlem79  46631  fourierdlem94  46646  fourierdlem113  46665  fouriersw  46677  fouriercn  46678  sge0isum  46873  hoicvr  46994  ovnsubaddlem2  47017  hoidmv1lelem1  47037  hoidmv1lelem3  47039  hoidmvlelem1  47041  hoidmvlelem4  47044  smflimlem2  47218  2timesltsq  47838  fmtnof1  48010  lighneallem2  48081  uspgrlim  48480  upgrwlkupwlk  48628  lincresunit3  48969  elbigolo1  49045  eenglngeehlnm  49227