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  3596  elovmpt3rab1  7628  smo11  8306  omeulem2  8520  oeeui  8540  oaabs2  8587  omabs  8589  omxpenlem  9018  map2xp  9087  mapdom2  9088  fsuppsssupp  9296  cantnflt  9593  cnfcom  9621  mapdjuen  10103  pwsdompw  10125  ackbij1lem5  10145  cofsmo  10191  fin1a2lem4  10325  ltmul12a  12009  lt2msq1  12038  ledivp1  12056  lemul1ad  12093  lemul2ad  12094  suprubd  12116  supaddc  12121  supadd  12122  supmul1  12123  supmul  12126  rpnnen1lem3  12904  rpnnen1lem5  12906  lediv2ad  12983  xaddge0  13185  xadddi  13222  xadddi2  13224  supicc  13429  supicclub  13431  difelfznle  13570  flval3  13747  expcan  14104  ltexp2  14105  ltexp2r  14108  expubnd  14113  ltexp2rd  14183  ltexp2d  14186  leexp2d  14187  expcand  14188  hashmap  14370  swrds1  14602  ccatswrd  14604  pfxfv  14618  swrdccatin1  14660  pfxccatin12lem3  14667  cshwidxmod  14738  wrdl3s3  14897  o1fsum  15748  mertenslem1  15819  eftlub  16046  rpnnen2lem4  16154  ruclem12  16178  dvdsadd  16241  3dvds  16270  divalgmod  16345  bitsmod  16375  bitsinv1lem  16380  bezoutlem4  16481  gcdzeq  16491  rplpwr  16497  sqgcd  16501  expgcd  16502  rpmulgcd2  16595  rpdvds  16599  coprmproddvdslem  16601  isprm5  16646  divgcdodd  16649  dvdszzq  16660  divnumden  16687  crth  16717  phimullem  16718  modprm0  16745  modprmn0modprm0  16747  coprimeprodsq2  16749  pythagtriplem19  16773  pockthlem  16845  prmunb  16854  prmreclem3  16858  prmreclem6  16861  ramub  16953  ramz  16965  kerf1ghm  19188  pmtrprfv  19394  pmtrprfv3  19395  mndodcong  19483  odngen  19518  pgpfi  19546  sylow2blem3  19563  lsmless1  19601  lsmless2  19602  lsmless12  19603  lsmmod2  19617  pj1id  19640  odadd2  19790  gexexlem  19793  ablfacrplem  20008  ablfacrp  20009  ablfac1b  20013  ablfac1eu  20016  pgpfac1lem2  20018  ogrpaddlt  20079  elrhmunit  20455  rrgnz  20649  ornglmullt  20814  orngrmullt  20815  lsmssspx  21052  lspsncv0  21113  znunit  21530  uvcvvcl2  21755  uvcvv1  21756  uvcvv0  21757  coe1subfv  22220  coe1fzgsumdlem  22259  scmate  22466  mdetunilem2  22569  pmatcoe1fsupp  22657  mat2pmatlin  22691  decpmatmullem  22727  pmatcollpw1lem1  22730  pmatcollpw1lem2  22731  pm2mpghm  22772  chpscmat  22798  chp0mat  22802  chpidmat  22803  cpmadugsumlemB  22830  cpmadugsumlemC  22831  cpmadugsumlemF  22832  clsndisj  23031  neiptopnei  23088  rnelfm  23909  fmfnfmlem2  23911  fmfnfm  23914  flimss1  23929  isfcf  23990  cnextfun  24020  cnextfvval  24021  cnextf  24022  cnextcn  24023  cnextfres1  24024  ustuqtop1  24197  utopsnneiplem  24203  xblss2ps  24357  xblss2  24358  stdbdxmet  24471  metcnpi3  24502  metustexhalf  24512  nmoi  24684  nmoi2  24686  nmoco  24693  blcvx  24754  icccmplem2  24780  icccmplem3  24781  reconnlem2  24784  xrge0gsumle  24790  metds0  24807  metdstri  24808  metdseq0  24811  lebnumlem3  24930  nmoleub2lem  25082  bcthlem5  25296  csschl  25344  minveclem2  25394  minveclem3b  25396  minveclem4  25400  minveclem6  25402  icombl  25533  cncombf  25627  mbflimsup  25635  itg2monolem1  25719  itg2cnlem1  25730  itg2cnlem2  25731  bddmulibl  25808  ellimc2  25846  cpnord  25905  cpnres  25907  dvmulbr  25909  dvmulbrOLD  25910  dvcobr  25917  dvcobrOLD  25918  dvlipcn  25967  dvlip2  25968  dvivthlem1  25981  lhop1lem  25986  lhop1  25987  dvfsumlem2  26001  dvfsumlem2OLD  26002  itgsubstlem  26023  deg1add  26076  deg1sublt  26083  ply1remlem  26138  plyeq0lem  26183  taylthlem2  26350  taylthlem2OLD  26351  ulmdvlem3  26379  abelthlem7  26416  pilem2  26430  pilem3  26431  pige3ALT  26497  logccv  26640  cxpaddlelem  26729  cvxcl  26963  fsumharmonic  26990  ftalem5  27055  mpodvdsmulf1o  27172  dvdsmulf1o  27174  bposlem1  27263  lgsqr  27330  lgsquad2lem2  27364  2lgsoddprmlem1  27387  2sqlem8a  27404  2sqlem8  27405  dchrmusum2  27473  dchrvmasumiflem1  27480  dchrisum0flblem1  27487  dchrisum0lem1b  27494  pntlem3  27588  noetasuplem4  27716  noetainflem4  27720  noetalem1  27721  divmulswd  28202  divsclwd  28204  uzsind  28413  tgdim01  28591  axsegcon  29012  ax5seglem1  29013  ax5seglem2  29014  axlowdimlem6  29032  axeuclidlem  29047  axcontlem7  29055  axcontlem9  29057  axcontlem10  29058  nbupgr  29429  nbumgrvtx  29431  cusgrsize2inds  29539  upgriswlk  29726  2pthnloop  29816  numclwwlk2lem1  30463  frgrreg  30481  nmoub3i  30860  ubthlem3  30959  minvecolem2  30962  minvecolem4  30967  minvecolem5  30968  minvecolem6  30969  htthlem  31004  pjpjpre  31506  chscllem1  31724  chscllem2  31725  chscllem3  31726  cnlnadjlem2  32155  leopnmid  32225  tpssad  32625  br8d  32697  swrdf1  33048  splfv3  33050  symgcom2  33177  cyc3genpmlem  33244  archirngz  33282  elrgspnlem1  33335  rlocf1  33366  subrdom  33378  dvdsruasso  33477  unitpidl1  33516  elrspunidl  33520  qsidomlem1  33544  ssdifidlprm  33550  mxidlirredi  33563  1arithidomlem2  33628  1arithidom  33629  1arithufdlem3  33638  ply1gsumz  33691  esplymhp  33744  esplyfvaln  33750  vietadeg1  33754  lssdimle  33784  dimkerim  33804  fedgmullem2  33807  fedgmul  33808  assalactf1o  33812  fldextrspundglemul  33856  fldextrspundgdvds  33858  minplyirred  33888  irredminply  33893  algextdeglem2  33895  rtelextdg2lem  33903  constrext2chnlem  33927  constrresqrtcl  33954  2sqr3minply  33957  cos9thpiminplylem2  33960  cos9thpiminply  33965  qqhval2lem  34158  qqhnm  34167  qqhucn  34169  esumcst  34240  esumpcvgval  34255  measunl  34393  dya2iocbrsiga  34452  dya2icobrsiga  34453  omssubadd  34477  inelcarsg  34488  carsgclctunlem2  34496  sibfof  34517  sitgaddlemb  34525  oddpwdc  34531  eulerpartlemgc  34539  bayesth  34616  ftc2re  34775  breprexplemc  34809  tgoldbachgt  34840  erdszelem8  35411  2goelgoanfmla1  35637  br8  35969  matunitlindflem2  37862  totbndbnd  38034  prdsbnd  38038  rrncmslem  38077  rrntotbnd  38081  isdrngo2  38203  lsatcmp  39373  lcvexchlem2  39405  lcvexchlem3  39406  ncvr1  39642  cvrletrN  39643  cvrnbtwn3  39646  cvrnrefN  39652  cvrcmp  39653  0ltat  39661  atnle0  39679  atlen0  39680  cvlcvr1  39709  cvrval3  39783  atle  39806  athgt  39826  1cvratex  39843  ps-2  39848  ps-2b  39852  llnnleat  39883  2atneat  39885  llnle  39888  atcvrlln  39890  llncmp  39892  2llnmat  39894  2at0mat0  39895  2atm  39897  ps-2c  39898  lplnle  39910  lplnnle2at  39911  llncvrlpln2  39927  llncvrlpln  39928  2lplnmN  39929  2llnmj  39930  2atmat  39931  lplncmp  39932  lplnexllnN  39934  2llnm2N  39938  2llnm4  39940  lvolnle3at  39952  4atlem3a  39967  4atlem3b  39968  4atlem10  39976  4atlem11  39979  4atlem12  39982  lplncvrlvol2  39985  lplncvrlvol  39986  lvolcmp  39987  2lplnm2N  39991  2lplnmj  39992  dalempjsen  40023  dalemcea  40030  dalem2  40031  dalemdea  40032  dalem9  40042  dalem16  40049  dalemcjden  40062  dalem21  40064  dalem23  40066  dalem39  40081  dalem54  40096  dalem60  40102  cdlemb  40164  elpadd2at  40176  paddasslem4  40193  paddasslem7  40196  paddasslem15  40204  paddasslem16  40205  pmodlem1  40216  pmodlem2  40217  llnexchb2  40239  pclfinclN  40320  osumcllem9N  40334  pmapojoinN  40338  pexmidN  40339  pl42lem1N  40349  lhp0lt  40373  lhpexle1  40378  lhpexle2lem  40379  lhpexle3lem  40381  lhprelat3N  40410  ltrnid  40505  trlval3  40557  arglem1N  40560  cdlemc5  40565  cdleme3b  40599  cdleme3c  40600  cdleme3h  40605  cdleme7e  40617  cdleme7ga  40618  cdleme20l1  40690  cdleme20l2  40691  cdleme20l  40692  cdleme22b  40711  cdlemefrs29clN  40769  cdlemefrs32fva  40770  cdlemeg46fvcl  40876  cdlemeg46c  40883  cdlemeg46fvaw  40886  cdlemeg46req  40899  cdleme48fgv  40908  cdlemf1  40931  cdlemg1cex  40958  cdlemg2dN  40960  cdlemg2ce  40962  cdlemg12e  41017  cdlemg35  41083  cdlemh  41187  tendocan  41194  cdlemk28-3  41278  tendoex  41345  dih1  41656  dihmeetlem9N  41685  dihlspsnssN  41702  dihlspsnat  41703  lcfrlem23  41935  renegneg  42776  fsuppind  42942  flt4lem4  43001  3cubes  43041  mzpsubst  43099  rencldnfi  43172  irrapx1  43179  pellexlem3  43182  pellexlem5  43184  infmrgelbi  43229  pellqrex  43230  pellfundge  43233  rmspecfund  43260  congtr  43316  acongeq  43334  jm2.20nn  43348  jm2.25lem1  43349  jm2.26  43353  expdiophlem1  43372  hbtlem2  43475  cantnftermord  43671  suprleubrd  44516  suprlubrd  44518  suprnmpt  45527  wessf1ornlem  45538  mpct  45553  upbdrech  45661  ssfiunibd  45665  uzfissfz  45679  xleadd2d  45680  suprltrp  45681  xleadd1d  45682  suprleubrnmpt  45774  iccintsng  45877  limcrecl  45983  fnlimfvre  46026  dvmulcncf  46277  dvdivcncf  46279  dvbdfbdioolem1  46280  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  stoweidlem1  46353  stoweidlem20  46372  stoweidlem24  46376  stoweidlem34  46386  stoweidlem45  46397  stoweidlem60  46412  fourierdlem20  46479  fourierdlem31  46490  fourierdlem38  46497  fourierdlem64  46522  fourierdlem79  46537  fourierdlem94  46552  fourierdlem113  46571  fouriersw  46583  fouriercn  46584  sge0isum  46779  hoicvr  46900  ovnsubaddlem2  46923  hoidmv1lelem1  46943  hoidmv1lelem3  46945  hoidmvlelem1  46947  hoidmvlelem4  46950  smflimlem2  47124  fmtnof1  47889  lighneallem2  47960  uspgrlim  48346  upgrwlkupwlk  48494  lincresunit3  48835  elbigolo1  48911  eenglngeehlnm  49093