Theorem syl31anc 1372

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

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

This theorem is referenced by:  syl32anc  1377  stoic4b  1779  elovmpt3rab1  7591  smo11  8265  omeulem2  8485  oeeui  8504  oaabs2  8550  omabs  8552  omxpenlem  8938  map2xp  9012  mapdom2  9013  fsuppsssupp  9242  cantnflt  9529  cnfcom  9557  mapdjuen  10037  pwsdompw  10061  ackbij1lem5  10081  cofsmo  10126  fin1a2lem4  10260  ltmul12a  11932  lt2msq1  11960  ledivp1  11978  lemul1ad  12015  lemul2ad  12016  suprubd  12038  supaddc  12043  supadd  12044  supmul1  12045  supmul  12048  rpnnen1lem3  12820  rpnnen1lem5  12822  lediv2ad  12895  xaddge0  13093  xadddi  13130  xadddi2  13132  supicc  13334  supicclub  13336  difelfznle  13471  flval3  13636  expcan  13988  ltexp2  13989  ltexp2r  13992  expubnd  13996  ltexp2rd  14064  ltexp2d  14069  leexp2d  14070  expcand  14071  hashmap  14250  swrds1  14477  ccatswrd  14479  pfxfv  14493  swrdccatin1  14536  pfxccatin12lem3  14543  cshwidxmod  14614  wrdl3s3  14776  o1fsum  15624  mertenslem1  15695  eftlub  15917  rpnnen2lem4  16025  ruclem12  16049  dvdsadd  16110  3dvds  16139  divalgmod  16214  bitsmod  16242  bitsinv1lem  16247  bezoutlem4  16349  gcdzeq  16359  rplpwr  16364  sqgcd  16367  rpmulgcd2  16458  rpdvds  16462  coprmproddvdslem  16464  isprm5  16509  divgcdodd  16512  divnumden  16549  crth  16576  phimullem  16577  modprm0  16603  modprmn0modprm0  16605  coprimeprodsq2  16607  pythagtriplem19  16631  pockthlem  16703  prmunb  16712  prmreclem3  16716  prmreclem6  16719  ramub  16811  ramz  16823  pmtrprfv  19157  pmtrprfv3  19158  mndodcong  19246  odngen  19278  pgpfi  19306  sylow2blem3  19323  lsmless1  19361  lsmless2  19362  lsmless12  19363  lsmmod2  19377  pj1id  19400  odadd2  19545  gexexlem  19548  ablfacrplem  19763  ablfacrp  19764  ablfac1b  19768  ablfac1eu  19771  pgpfac1lem2  19773  kerf1ghm  20085  elrhmunit  20091  lsmssspx  20456  lspsncv0  20514  znunit  20877  uvcvvcl2  21101  uvcvv1  21102  uvcvv0  21103  coe1subfv  21543  coe1fzgsumdlem  21578  scmate  21765  mdetunilem2  21868  pmatcoe1fsupp  21956  mat2pmatlin  21990  decpmatmullem  22026  pmatcollpw1lem1  22029  pmatcollpw1lem2  22030  pm2mpghm  22071  chpscmat  22097  chp0mat  22101  chpidmat  22102  cpmadugsumlemB  22129  cpmadugsumlemC  22130  cpmadugsumlemF  22131  clsndisj  22332  neiptopnei  22389  rnelfm  23210  fmfnfmlem2  23212  fmfnfm  23215  flimss1  23230  isfcf  23291  cnextfun  23321  cnextfvval  23322  cnextf  23323  cnextcn  23324  cnextfres1  23325  ustuqtop1  23499  utopsnneiplem  23505  xblss2ps  23660  xblss2  23661  stdbdxmet  23777  metcnpi3  23808  metustexhalf  23818  nmoi  23998  nmoi2  24000  nmoco  24007  blcvx  24067  icccmplem2  24092  icccmplem3  24093  reconnlem2  24096  xrge0gsumle  24102  metds0  24119  metdstri  24120  metdseq0  24123  lebnumlem3  24232  nmoleub2lem  24383  bcthlem5  24598  csschl  24646  minveclem2  24696  minveclem3b  24698  minveclem4  24702  minveclem6  24704  icombl  24834  cncombf  24928  mbflimsup  24936  itg2monolem1  25021  itg2cnlem1  25032  itg2cnlem2  25033  bddmulibl  25109  ellimc2  25147  cpnord  25205  cpnres  25207  dvmulbr  25209  dvcobr  25216  dvlipcn  25264  dvlip2  25265  dvivthlem1  25278  lhop1lem  25283  lhop1  25284  dvfsumlem2  25297  itgsubstlem  25318  deg1add  25374  deg1sublt  25381  ply1remlem  25433  plyeq0lem  25477  taylthlem2  25639  ulmdvlem3  25667  abelthlem7  25703  pilem2  25717  pilem3  25718  pige3ALT  25782  logccv  25924  cxpaddlelem  26010  cvxcl  26240  fsumharmonic  26267  ftalem5  26332  dvdsmulf1o  26449  bposlem1  26538  lgsqr  26605  lgsquad2lem2  26639  2lgsoddprmlem1  26662  2sqlem8a  26679  2sqlem8  26680  dchrmusum2  26748  dchrvmasumiflem1  26755  dchrisum0flblem1  26762  dchrisum0lem1b  26769  pntlem3  26863  noetasuplem4  26990  noetainflem4  26994  noetalem1  26995  tgdim01  27157  axsegcon  27584  ax5seglem1  27585  ax5seglem2  27586  axlowdimlem6  27604  axeuclidlem  27619  axcontlem7  27627  axcontlem9  27629  axcontlem10  27630  nbupgr  28000  nbumgrvtx  28002  cusgrsize2inds  28109  upgriswlk  28297  2pthnloop  28387  numclwwlk2lem1  29028  frgrreg  29046  nmoub3i  29423  ubthlem3  29522  minvecolem2  29525  minvecolem4  29530  minvecolem5  29531  minvecolem6  29532  htthlem  29567  pjpjpre  30069  chscllem1  30287  chscllem2  30288  chscllem3  30289  cnlnadjlem2  30718  leopnmid  30788  br8d  31237  dvdszzq  31416  swrdf1  31515  splfv3  31517  ogrpaddlt  31630  symgcom2  31640  cyc3genpmlem  31705  archirngz  31730  ornglmullt  31806  orngrmullt  31807  elrspunidl  31903  qsidomlem1  31925  lssdimle  31989  dimkerim  32006  fedgmullem2  32009  fedgmul  32010  qqhval2lem  32229  qqhnm  32238  qqhucn  32240  esumcst  32329  esumpcvgval  32344  measunl  32482  dya2iocbrsiga  32542  dya2icobrsiga  32543  omssubadd  32567  inelcarsg  32578  carsgclctunlem2  32586  sibfof  32607  sitgaddlemb  32615  oddpwdc  32621  eulerpartlemgc  32629  bayesth  32706  ftc2re  32878  breprexplemc  32912  tgoldbachgt  32943  erdszelem8  33459  2goelgoanfmla1  33685  br8  34012  matunitlindflem2  35887  totbndbnd  36060  prdsbnd  36064  rrncmslem  36103  rrntotbnd  36107  isdrngo2  36229  lsatcmp  37278  lcvexchlem2  37310  lcvexchlem3  37311  ncvr1  37547  cvrletrN  37548  cvrnbtwn3  37551  cvrnrefN  37557  cvrcmp  37558  0ltat  37566  atnle0  37584  atlen0  37585  cvlcvr1  37614  cvrval3  37689  atle  37712  athgt  37732  1cvratex  37749  ps-2  37754  ps-2b  37758  llnnleat  37789  2atneat  37791  llnle  37794  atcvrlln  37796  llncmp  37798  2llnmat  37800  2at0mat0  37801  2atm  37803  ps-2c  37804  lplnle  37816  lplnnle2at  37817  llncvrlpln2  37833  llncvrlpln  37834  2lplnmN  37835  2llnmj  37836  2atmat  37837  lplncmp  37838  lplnexllnN  37840  2llnm2N  37844  2llnm4  37846  lvolnle3at  37858  4atlem3a  37873  4atlem3b  37874  4atlem10  37882  4atlem11  37885  4atlem12  37888  lplncvrlvol2  37891  lplncvrlvol  37892  lvolcmp  37893  2lplnm2N  37897  2lplnmj  37898  dalempjsen  37929  dalemcea  37936  dalem2  37937  dalemdea  37938  dalem9  37948  dalem16  37955  dalemcjden  37968  dalem21  37970  dalem23  37972  dalem39  37987  dalem54  38002  dalem60  38008  cdlemb  38070  elpadd2at  38082  paddasslem4  38099  paddasslem7  38102  paddasslem15  38110  paddasslem16  38111  pmodlem1  38122  pmodlem2  38123  llnexchb2  38145  pclfinclN  38226  osumcllem9N  38240  pmapojoinN  38244  pexmidN  38245  pl42lem1N  38255  lhp0lt  38279  lhpexle1  38284  lhpexle2lem  38285  lhpexle3lem  38287  lhprelat3N  38316  ltrnid  38411  trlval3  38463  arglem1N  38466  cdlemc5  38471  cdleme3b  38505  cdleme3c  38506  cdleme3h  38511  cdleme7e  38523  cdleme7ga  38524  cdleme20l1  38596  cdleme20l2  38597  cdleme20l  38598  cdleme22b  38617  cdlemefrs29clN  38675  cdlemefrs32fva  38676  cdlemeg46fvcl  38782  cdlemeg46c  38789  cdlemeg46fvaw  38792  cdlemeg46req  38805  cdleme48fgv  38814  cdlemf1  38837  cdlemg1cex  38864  cdlemg2dN  38866  cdlemg2ce  38868  cdlemg12e  38923  cdlemg35  38989  cdlemh  39093  tendocan  39100  cdlemk28-3  39184  tendoex  39251  dih1  39562  dihmeetlem9N  39591  dihlspsnssN  39608  dihlspsnat  39609  lcfrlem23  39841  3rspcedvdw  40446  fsuppind  40547  expgcd  40602  renegneg  40662  flt4lem4  40756  3cubes  40782  mzpsubst  40840  rencldnfi  40913  irrapx1  40920  pellexlem3  40923  pellexlem5  40925  infmrgelbi  40970  pellqrex  40971  pellfundge  40974  rmspecfund  41001  congtr  41058  acongeq  41076  jm2.20nn  41090  jm2.25lem1  41091  jm2.26  41095  expdiophlem1  41114  hbtlem2  41220  suprleubrd  42106  suprlubrd  42108  suprnmpt  43045  wessf1ornlem  43057  mpct  43076  upbdrech  43187  ssfiunibd  43191  uzfissfz  43208  xleadd2d  43209  suprltrp  43210  xleadd1d  43211  suprleubrnmpt  43305  iccintsng  43405  limcrecl  43514  fnlimfvre  43559  dvmulcncf  43810  dvdivcncf  43812  dvbdfbdioolem1  43813  ioodvbdlimc1lem2  43817  ioodvbdlimc2lem  43819  stoweidlem1  43886  stoweidlem20  43905  stoweidlem24  43909  stoweidlem34  43919  stoweidlem45  43930  stoweidlem60  43945  fourierdlem20  44012  fourierdlem31  44023  fourierdlem38  44030  fourierdlem64  44055  fourierdlem79  44070  fourierdlem94  44085  fourierdlem113  44104  fouriersw  44116  fouriercn  44117  sge0isum  44310  hoicvr  44431  ovnsubaddlem2  44454  hoidmv1lelem1  44474  hoidmv1lelem3  44476  hoidmvlelem1  44478  hoidmvlelem4  44481  smflimlem2  44655  fmtnof1  45346  lighneallem2  45417  upgrwlkupwlk  45661  lincresunit3  46181  elbigolo1  46262  eenglngeehlnm  46444