Theorem syl31anc 1396

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl32anc  1401  stoic4b  1801  3rspcedvdw  3602  elovmpt3rab1  7660  smo11  8339  omeulem2  8556  oeeui  8576  oaabs2  8623  omabs  8625  omxpenlem  9054  map2xp  9123  mapdom2  9124  fsuppsssupp  9329  cantnflt  9629  cnfcom  9657  mapdjuen  10152  pwsdompw  10174  ackbij1lem5  10194  cofsmo  10241  fin1a2lem4  10375  ltmul12a  12062  lt2msq1  12090  ledivp1  12108  lemul1ad  12145  lemul2ad  12146  suprubd  12168  supaddc  12173  supadd  12174  supmul1  12175  supmul  12178  rpnnen1lem3  12994  rpnnen1lem5  12996  lediv2ad  13073  xaddge0  13275  xadddi  13312  xadddi2  13314  supicc  13519  supicclub  13521  difelfznle  13661  flval3  13839  expcan  14196  ltexp2  14197  ltexp2r  14200  expubnd  14205  ltexp2rd  14275  ltexp2d  14278  leexp2d  14279  expcand  14280  hashmap  14462  swrds1  14694  ccatswrd  14696  pfxfv  14710  swrdccatin1  14752  pfxccatin12lem3  14759  cshwidxmod  14830  wrdl3s3  14989  o1fsum  15855  mertenslem1  15928  eftlub  16155  rpnnen2lem4  16263  ruclem12  16287  dvdsadd  16350  3dvds  16379  divalgmod  16454  bitsmod  16484  bitsinv1lem  16489  bezoutlem4  16590  gcdzeq  16600  rplpwr  16606  sqgcd  16610  expgcd  16611  rpmulgcd2  16704  rpdvds  16708  coprmproddvdslem  16710  isprm5  16756  divgcdodd  16759  dvdszzq  16770  divnumden  16797  crth  16827  phimullem  16828  modprm0  16855  modprmn0modprm0  16857  coprimeprodsq2  16859  pythagtriplem19  16883  pockthlem  16955  prmunb  16964  prmreclem3  16968  prmreclem6  16971  ramub  17063  ramz  17075  kerf1ghm  19308  pmtrprfv  19514  pmtrprfv3  19515  mndodcong  19603  odngen  19638  pgpfi  19666  sylow2blem3  19683  lsmless1  19721  lsmless2  19722  lsmless12  19723  lsmmod2  19737  pj1id  19760  odadd2  19910  gexexlem  19913  ablfacrplem  20128  ablfacrp  20129  ablfac1b  20133  ablfac1eu  20136  pgpfac1lem2  20138  ogrpaddlt  20199  elrhmunit  20584  rrgnz  20780  ornglmullt  20941  orngrmullt  20942  lsmssspx  21178  lspsncv0  21239  qsidomlem1  21440  ssdifidlprm  21446  znunit  21673  uvcvvcl2  21898  uvcvv1  21899  uvcvv0  21900  coe1subfv  22387  coe1fzgsumdlem  22424  scmate  22628  mdetunilem2  22731  pmatcoe1fsupp  22819  mat2pmatlin  22853  decpmatmullem  22889  pmatcollpw1lem1  22892  pmatcollpw1lem2  22893  pm2mpghm  22934  chpscmat  22960  chp0mat  22964  chpidmat  22965  cpmadugsumlemB  22992  cpmadugsumlemC  22993  cpmadugsumlemF  22994  clsndisj  23193  neiptopnei  23250  rnelfm  24071  fmfnfmlem2  24073  fmfnfm  24076  flimss1  24091  isfcf  24152  cnextfun  24182  cnextfvval  24183  cnextf  24184  cnextcn  24185  cnextfres1  24186  ustuqtop1  24359  utopsnneiplem  24365  xblss2ps  24519  xblss2  24520  stdbdxmet  24633  metcnpi3  24664  metustexhalf  24674  nmoi  24846  nmoi2  24848  nmoco  24855  blcvx  24916  icccmplem2  24942  icccmplem3  24943  reconnlem2  24946  xrge0gsumle  24952  metds0  24969  metdstri  24970  metdseq0  24973  lebnumlem3  25083  nmoleub2lem  25234  bcthlem5  25448  csschl  25496  minveclem2  25546  minveclem3b  25548  minveclem4  25552  minveclem6  25554  icombl  25684  cncombf  25778  mbflimsup  25786  itg2monolem1  25870  itg2cnlem1  25881  itg2cnlem2  25882  bddmulibl  25959  ellimc2  25997  cpnord  26055  cpnres  26057  dvmulbr  26059  dvcobr  26066  dvlipcn  26114  dvlip2  26115  dvivthlem1  26128  lhop1lem  26133  lhop1  26134  dvfsumlem2  26147  itgsubstlem  26168  deg1add  26221  deg1sublt  26228  ply1remlem  26283  plyeq0lem  26328  taylthlem2  26495  ulmdvlem3  26523  abelthlem7  26559  pilem2  26573  pilem3  26574  pige3ALT  26643  logccv  26786  cxpaddlelem  26874  cvxcl  27107  fsumharmonic  27134  ftalem5  27199  mpodvdsmulf1o  27316  dvdsmulf1o  27318  bposlem1  27406  lgsqr  27473  lgsquad2lem2  27507  2lgsoddprmlem1  27530  2sqlem8a  27547  2sqlem8  27548  dchrmusum2  27616  dchrvmasumiflem1  27623  dchrisum0flblem1  27630  dchrisum0lem1b  27637  pntlem3  27731  noetasuplem4  27858  noetainflem4  27862  noetalem1  27863  divmulswd  28345  divsclwd  28347  uzsind  28556  tgdim01  28734  axsegcon  29186  ax5seglem1  29187  ax5seglem2  29188  axlowdimlem6  29206  axeuclidlem  29221  axcontlem7  29229  axcontlem9  29231  axcontlem10  29232  nbupgr  29603  nbumgrvtx  29605  cusgrsize2inds  29712  upgriswlk  29899  2pthnloop  29989  numclwwlk2lem1  30636  frgrreg  30654  nmoub3i  31034  ubthlem3  31133  minvecolem2  31136  minvecolem4  31141  minvecolem5  31142  minvecolem6  31143  htthlem  31178  pjpjpre  31680  chscllem1  31898  chscllem2  31899  chscllem3  31900  cnlnadjlem2  32329  leopnmid  32399  tpssad  32795  br8d  32865  swrdf1  33189  splfv3  33191  symgcom2  33317  cyc3genpmlem  33384  archirngz  33422  elrgspnlem1  33475  erld2  33499  rlocf1  33507  subrdom  33518  ricdomn1  33522  dvdsruasso  33614  unitpidl1  33648  elrspunidl  33652  mxidlirredi  33671  dflringlem2  33702  1arithidomlem2  33743  1arithidom  33744  1arithufdlem3  33753  ply1gsumz  33806  mplidomlem  33834  esplymhp  33875  esplyfvaln  33881  vietadeg1  33885  lssdimle  33915  dimkerim  33934  fedgmullem2  33937  fedgmul  33938  assalactf1o  33942  fldextrspundglemul  33986  fldextrspundgdvds  33988  minplyirred  34018  irredminply  34023  algextdeglem2  34025  rtelextdg2lem  34033  constrext2chnlem  34057  constrresqrtcl  34084  2sqr3minply  34087  cos9thpiminplylem2  34090  cos9thpiminply  34095  qqhval2lem  34288  qqhnm  34297  qqhucn  34299  esumcst  34370  esumpcvgval  34385  measunl  34523  dya2iocbrsiga  34582  dya2icobrsiga  34583  omssubadd  34607  inelcarsg  34618  carsgclctunlem2  34626  sibfof  34647  sitgaddlemb  34655  oddpwdc  34661  eulerpartlemgc  34669  bayesth  34746  ftc2re  34902  breprexplemc  34936  tgoldbachgt  34967  erdszelem8  35561  2goelgoanfmla1  35787  br8  36119  matunitlindflem2  38128  totbndbnd  38300  prdsbnd  38304  rrncmslem  38343  rrntotbnd  38347  isdrngo2  38469  lsatcmp  39639  lcvexchlem2  39671  lcvexchlem3  39672  ncvr1  39908  cvrletrN  39909  cvrnbtwn3  39912  cvrnrefN  39918  cvrcmp  39919  0ltat  39927  atnle0  39945  atlen0  39946  cvlcvr1  39975  cvrval3  40049  atle  40072  athgt  40092  1cvratex  40109  ps-2  40114  ps-2b  40118  llnnleat  40149  2atneat  40151  llnle  40154  atcvrlln  40156  llncmp  40158  2llnmat  40160  2at0mat0  40161  2atm  40163  ps-2c  40164  lplnle  40176  lplnnle2at  40177  llncvrlpln2  40193  llncvrlpln  40194  2lplnmN  40195  2llnmj  40196  2atmat  40197  lplncmp  40198  lplnexllnN  40200  2llnm2N  40204  2llnm4  40206  lvolnle3at  40218  4atlem3a  40233  4atlem3b  40234  4atlem10  40242  4atlem11  40245  4atlem12  40248  lplncvrlvol2  40251  lplncvrlvol  40252  lvolcmp  40253  2lplnm2N  40257  2lplnmj  40258  dalempjsen  40289  dalemcea  40296  dalem2  40297  dalemdea  40298  dalem9  40308  dalem16  40315  dalemcjden  40328  dalem21  40330  dalem23  40332  dalem39  40347  dalem54  40362  dalem60  40368  cdlemb  40430  elpadd2at  40442  paddasslem4  40459  paddasslem7  40462  paddasslem15  40470  paddasslem16  40471  pmodlem1  40482  pmodlem2  40483  llnexchb2  40505  pclfinclN  40586  osumcllem9N  40600  pmapojoinN  40604  pexmidN  40605  pl42lem1N  40615  lhp0lt  40639  lhpexle1  40644  lhpexle2lem  40645  lhpexle3lem  40647  lhprelat3N  40676  ltrnid  40771  trlval3  40823  arglem1N  40826  cdlemc5  40831  cdleme3b  40865  cdleme3c  40866  cdleme3h  40871  cdleme7e  40883  cdleme7ga  40884  cdleme20l1  40956  cdleme20l2  40957  cdleme20l  40958  cdleme22b  40977  cdlemefrs29clN  41035  cdlemefrs32fva  41036  cdlemeg46fvcl  41142  cdlemeg46c  41149  cdlemeg46fvaw  41152  cdlemeg46req  41165  cdleme48fgv  41174  cdlemf1  41197  cdlemg1cex  41224  cdlemg2dN  41226  cdlemg2ce  41228  cdlemg12e  41283  cdlemg35  41349  cdlemh  41453  tendocan  41460  cdlemk28-3  41544  tendoex  41611  dih1  41922  dihmeetlem9N  41951  dihlspsnssN  41968  dihlspsnat  41969  lcfrlem23  42201  renegneg  43033  fsuppind  43184  flt4lem4  43243  3cubes  43283  mzpsubst  43341  rencldnfi  43410  irrapx1  43417  pellexlem3  43420  pellexlem5  43422  infmrgelbi  43467  pellqrex  43468  pellfundge  43471  rmspecfund  43498  congtr  43554  acongeq  43572  jm2.20nn  43586  jm2.25lem1  43587  jm2.26  43591  expdiophlem1  43610  hbtlem2  43713  cantnftermord  43909  suprleubrd  44754  suprlubrd  44756  suprnmpt  45750  wessf1ornlem  45761  mpct  45776  upbdrech  45882  ssfiunibd  45886  uzfissfz  45900  xleadd2d  45901  suprltrp  45902  xleadd1d  45903  suprleubrnmpt  45994  iccintsng  46097  limcrecl  46203  fnlimfvre  46246  dvmulcncf  46497  dvdivcncf  46499  dvbdfbdioolem1  46500  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  stoweidlem1  46573  stoweidlem20  46592  stoweidlem24  46596  stoweidlem34  46606  stoweidlem45  46617  stoweidlem60  46632  fourierdlem20  46699  fourierdlem31  46710  fourierdlem38  46717  fourierdlem64  46742  fourierdlem79  46757  fourierdlem94  46772  fourierdlem113  46791  fouriersw  46803  fouriercn  46804  sge0isum  46999  hoicvr  47120  ovnsubaddlem2  47143  hoidmv1lelem1  47163  hoidmv1lelem3  47165  hoidmvlelem1  47167  hoidmvlelem4  47170  smflimlem2  47344  2timesltsq  47970  fmtnof1  48142  lighneallem2  48213  uspgrlim  48612  upgrwlkupwlk  48760  lincresunit3  49112  elbigolo1  49188  eenglngeehlnm  49370