Theorem syl31anc 1400

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl32anc  1405  stoic4b  1811  3rspcedvdw  3597  elovmpt3rab1  7678  smo11  8357  omeulem2  8574  oeeui  8594  oaabs2  8641  omabs  8643  omxpenlem  9080  map2xp  9149  mapdom2  9150  fsuppsssupp  9355  cantnflt  9655  cnfcom  9683  mapdjuen  10187  pwsdompw  10209  ackbij1lem5  10229  cofsmo  10275  fin1a2lem4  10409  ltmul12a  12099  lt2msq1  12127  ledivp1  12145  lemul1ad  12182  lemul2ad  12183  suprubd  12205  supaddc  12210  supadd  12211  supmul1  12212  supmul  12215  rpnnen1lem3  13033  rpnnen1lem5  13035  lediv2ad  13112  xaddge0  13314  xadddi  13351  xadddi2  13353  supicc  13558  supicclub  13560  difelfznle  13701  flval3  13880  expcan  14237  ltexp2  14238  ltexp2r  14241  expubnd  14246  ltexp2rd  14316  ltexp2d  14319  leexp2d  14320  expcand  14321  hashmap  14504  swrdf1  14723  swrds1  14740  ccatswrd  14742  pfxfv  14756  swrdccatin1  14798  pfxccatin12lem3  14805  cshwidxmod  14878  wrdl3s3  15039  o1fsum  15904  mertenslem1  15977  eftlub  16203  rpnnen2lem4  16311  ruclem12  16335  dvdsadd  16398  3dvds  16427  divalgmod  16502  bitsmod  16532  bitsinv1lem  16537  bezoutlem4  16638  gcdzeq  16648  rplpwr  16654  sqgcd  16658  expgcd  16659  rpmulgcd2  16752  rpdvds  16756  coprmproddvdslem  16758  isprm5  16804  divgcdodd  16807  dvdszzq  16818  divnumden  16845  crth  16875  phimullem  16876  modprm0  16903  modprmn0modprm0  16905  coprimeprodsq2  16907  pythagtriplem19  16931  pockthlem  17003  prmunb  17012  prmreclem3  17016  prmreclem6  17019  ramub  17111  ramz  17123  kerf1ghm  19380  pmtrprfv  19586  pmtrprfv3  19587  mndodcong  19675  odngen  19710  pgpfi  19738  sylow2blem3  19755  lsmless1  19793  lsmless2  19794  lsmless12  19795  lsmmod2  19809  pj1id  19832  odadd2  19982  gexexlem  19985  ablfacrplem  20200  ablfacrp  20201  ablfac1b  20205  ablfac1eu  20208  pgpfac1lem2  20210  ogrpaddlt  20271  elrhmunit  20676  rrgnz  20872  ornglmullt  21041  orngrmullt  21042  lsmssspx  21278  lspsncv0  21339  qsidomlem1  21549  ssdifidlprm  21555  znunit  21782  uvcvvcl2  22007  uvcvv1  22008  uvcvv0  22009  coe1subfv  22498  coe1fzgsumdlem  22534  scmate  22738  mdetunilem2  22841  matunitlindflem2  22908  pmatcoe1fsupp  22932  mat2pmatlin  22966  decpmatmullem  23002  pmatcollpw1lem1  23005  pmatcollpw1lem2  23006  pm2mpghm  23047  chpscmat  23073  chp0mat  23077  chpidmat  23078  cpmadugsumlemB  23105  cpmadugsumlemC  23106  cpmadugsumlemF  23107  clsndisj  23306  neiptopnei  23363  rnelfm  24185  fmfnfmlem2  24187  fmfnfm  24190  flimss1  24205  isfcf  24266  cnextfun  24296  cnextfvval  24297  cnextf  24298  cnextcn  24299  cnextfres1  24300  ustuqtop1  24473  utopsnneiplem  24479  xblss2ps  24633  xblss2  24634  stdbdxmet  24747  metcnpi3  24778  metustexhalf  24788  nmoi  24960  nmoi2  24962  nmoco  24969  blcvx  25030  icccmplem2  25056  icccmplem3  25057  reconnlem2  25060  xrge0gsumle  25066  metds0  25083  metdstri  25084  metdseq0  25087  lebnumlem3  25197  nmoleub2lem  25348  bcthlem5  25562  csschl  25610  minveclem2  25660  minveclem3b  25662  minveclem4  25666  minveclem6  25668  icombl  25798  cncombf  25892  mbflimsup  25900  itg2monolem1  25984  itg2cnlem1  25995  itg2cnlem2  25996  bddmulibl  26073  ellimc2  26111  cpnord  26169  cpnres  26171  dvmulbr  26173  dvcobr  26180  dvlipcn  26228  dvlip2  26229  dvivthlem1  26242  lhop1lem  26247  lhop1  26248  dvfsumlem2  26261  itgsubstlem  26282  deg1add  26335  deg1sublt  26342  ply1remlem  26397  plyeq0lem  26443  taylthlem2  26617  ulmdvlem3  26645  abelthlem7  26681  pilem2  26695  pilem3  26696  pige3ALT  26765  logccv  26908  cxpaddlelem  26996  cvxcl  27229  fsumharmonic  27256  ftalem5  27321  mpodvdsmulf1o  27438  dvdsmulf1o  27440  bposlem1  27528  lgsqr  27595  lgsquad2lem2  27629  2lgsoddprmlem1  27652  2sqlem8a  27669  2sqlem8  27670  dchrmusum2  27738  dchrvmasumiflem1  27745  dchrisum0flblem1  27752  dchrisum0lem1b  27759  pntlem3  27853  noetasuplem4  27980  noetainflem4  27984  noetalem1  27985  divmulswd  28467  divsclwd  28469  uzsind  28678  tgdim01  28857  axsegcon  29392  ax5seglem1  29393  ax5seglem2  29394  axlowdimlem6  29412  axeuclidlem  29427  axcontlem7  29435  axcontlem9  29437  axcontlem10  29438  nbupgr  29812  nbumgrvtx  29814  cusgrsize2inds  29921  upgriswlk  30108  2pthnloop  30204  numclwwlk2lem1  30864  frgrreg  30882  nmoub3i  31262  ubthlem3  31361  minvecolem2  31364  minvecolem4  31369  minvecolem5  31370  minvecolem6  31371  htthlem  31406  pjpjpre  31908  chscllem1  32126  chscllem2  32127  chscllem3  32128  cnlnadjlem2  32557  leopnmid  32627  tpssad  33022  br8d  33089  splfv3  33406  symgcom2  33532  cyc3genpmlem  33599  archirngz  33637  elrgspnlem1  33690  erld2  33714  rlocf1  33722  subrdom  33733  ricdomn1  33737  dvdsruasso  33826  unitpidl1  33860  elrspunidl  33864  mxidlirredi  33882  dflringlem2  33913  1arithidomlem2  33954  1arithidom  33955  1arithufdlem3  33964  ply1gsumz  34017  mplidomlem  34045  esplymhp  34086  esplyfvaln  34092  vietadeg1  34096  lssdimle  34126  dimkerim  34145  fedgmullem2  34148  fedgmul  34149  assalactf1o  34153  fldextrspundglemul  34197  fldextrspundgdvds  34199  minplyirred  34229  irredminply  34234  algextdeglem2  34236  rtelextdg2lem  34244  constrext2chnlem  34268  constrresqrtcl  34295  2sqr3minply  34298  cos9thpiminplylem2  34301  cos9thpiminply  34306  qqhval2lem  34499  qqhnm  34508  qqhucn  34510  esumcst  34581  esumpcvgval  34596  measunl  34735  dya2iocbrsiga  34794  dya2icobrsiga  34795  omssubadd  34819  inelcarsg  34830  carsgclctunlem2  34838  sibfof  34859  sitgaddlemb  34867  oddpwdc  34873  eulerpartlemgc  34881  bayesth  34958  ftc2re  35114  breprexplemc  35148  tgoldbachgt  35179  erdszelem8  35785  2goelgoanfmla1  36011  br8  36343  totbndbnd  38547  prdsbnd  38551  rrncmslem  38590  rrntotbnd  38594  isdrngo2  38716  lsatcmp  39884  lcvexchlem2  39916  lcvexchlem3  39917  ncvr1  40153  cvrletrN  40154  cvrnbtwn3  40157  cvrnrefN  40163  cvrcmp  40164  0ltat  40172  atnle0  40190  atlen0  40191  cvlcvr1  40220  cvrval3  40294  atle  40317  athgt  40337  1cvratex  40354  ps-2  40359  ps-2b  40363  llnnleat  40394  2atneat  40396  llnle  40399  atcvrlln  40401  llncmp  40403  2llnmat  40405  2at0mat0  40406  2atm  40408  ps-2c  40409  lplnle  40421  lplnnle2at  40422  llncvrlpln2  40438  llncvrlpln  40439  2lplnmN  40440  2llnmj  40441  2atmat  40442  lplncmp  40443  lplnexllnN  40445  2llnm2N  40449  2llnm4  40451  lvolnle3at  40463  4atlem3a  40478  4atlem3b  40479  4atlem10  40487  4atlem11  40490  4atlem12  40493  lplncvrlvol2  40496  lplncvrlvol  40497  lvolcmp  40498  2lplnm2N  40502  2lplnmj  40503  dalempjsen  40534  dalemcea  40541  dalem2  40542  dalemdea  40543  dalem9  40553  dalem16  40560  dalemcjden  40573  dalem21  40575  dalem23  40577  dalem39  40592  dalem54  40607  dalem60  40613  cdlemb  40675  elpadd2at  40687  paddasslem4  40704  paddasslem7  40707  paddasslem15  40715  paddasslem16  40716  pmodlem1  40727  pmodlem2  40728  llnexchb2  40750  pclfinclN  40831  osumcllem9N  40845  pmapojoinN  40849  pexmidN  40850  pl42lem1N  40860  lhp0lt  40884  lhpexle1  40889  lhpexle2lem  40890  lhpexle3lem  40892  lhprelat3N  40921  ltrnid  41016  trlval3  41068  arglem1N  41071  cdlemc5  41076  cdleme3b  41110  cdleme3c  41111  cdleme3h  41116  cdleme7e  41128  cdleme7ga  41129  cdleme20l1  41201  cdleme20l2  41202  cdleme20l  41203  cdleme22b  41222  cdlemefrs29clN  41280  cdlemefrs32fva  41281  cdlemeg46fvcl  41387  cdlemeg46c  41394  cdlemeg46fvaw  41397  cdlemeg46req  41410  cdleme48fgv  41419  cdlemf1  41442  cdlemg1cex  41469  cdlemg2dN  41471  cdlemg2ce  41473  cdlemg12e  41528  cdlemg35  41594  cdlemh  41698  tendocan  41705  cdlemk28-3  41789  tendoex  41856  dih1  42167  dihmeetlem9N  42196  dihlspsnssN  42213  dihlspsnat  42214  lcfrlem23  42446  renegneg  43295  fsuppind  43444  flt4lem4  43503  3cubes  43543  mzpsubst  43601  rencldnfi  43670  irrapx1  43677  pellexlem3  43680  pellexlem5  43682  infmrgelbi  43727  pellqrex  43728  pellfundge  43731  rmspecfund  43758  congtr  43814  acongeq  43832  jm2.20nn  43846  jm2.25lem1  43847  jm2.26  43851  expdiophlem1  43870  hbtlem2  43973  cantnftermord  44169  suprleubrd  45014  suprlubrd  45016  suprnmpt  46014  wessf1ornlem  46025  mpct  46040  upbdrech  46146  ssfiunibd  46150  uzfissfz  46164  xleadd2d  46165  suprltrp  46166  xleadd1d  46167  suprleubrnmpt  46258  iccintsng  46361  limcrecl  46467  fnlimfvre  46510  dvmulcncf  46761  dvdivcncf  46763  dvbdfbdioolem1  46764  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  stoweidlem1  46837  stoweidlem20  46856  stoweidlem24  46860  stoweidlem34  46870  stoweidlem45  46881  stoweidlem60  46896  fourierdlem20  46963  fourierdlem31  46974  fourierdlem38  46981  fourierdlem64  47006  fourierdlem79  47021  fourierdlem94  47036  fourierdlem113  47055  fouriersw  47067  fouriercn  47068  sge0isum  47263  hoicvr  47384  ovnsubaddlem2  47407  hoidmv1lelem1  47427  hoidmv1lelem3  47429  hoidmvlelem1  47431  hoidmvlelem4  47434  smflimlem2  47608  2timesltsq  48274  fmtnof1  48446  lighneallem2  48517  uspgrlim  48916  upgrwlkupwlk  49064  lincresunit3  49419  elbigolo1  49495  eenglngeehlnm  49677