Theorem syl31anc 1401

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  1406  stoic4b  1811  3rspcedvdw  3597  elovmpt3rab1  7708  smo11  8403  omeulem2  8622  oeeui  8642  oaabs2  8689  omabs  8691  omxpenlem  9128  map2xp  9197  mapdom2  9198  fsuppsssupp  9403  cantnflt  9703  cnfcom  9731  mapdjuen  10289  pwsdompw  10311  ackbij1lem5  10331  cofsmo  10377  fin1a2lem4  10511  ltmul12a  12203  lt2msq1  12231  ledivp1  12249  lemul1ad  12286  lemul2ad  12287  suprubd  12309  supaddc  12314  supadd  12315  supmul1  12316  supmul  12319  rpnnen1lem3  13137  rpnnen1lem5  13139  lediv2ad  13216  xaddge0  13418  xadddi  13455  xadddi2  13457  supicc  13662  supicclub  13664  difelfznle  13806  flval3  13985  expcan  14342  ltexp2  14343  ltexp2r  14346  expubnd  14351  ltexp2rd  14422  ltexp2d  14425  leexp2d  14426  expcand  14427  hashmap  14610  swrdf1  14830  swrds1  14847  ccatswrd  14849  pfxfv  14863  swrdccatin1  14905  pfxccatin12lem3  14912  cshwidxmod  14985  wrdl3s3  15147  o1fsum  16012  mertenslem1  16085  eftlub  16309  rpnnen2lem4  16417  ruclem12  16441  dvdsadd  16504  3dvds  16533  divalgmod  16608  bitsmod  16638  bitsinv1lem  16643  bezoutlem4  16747  gcdzeq  16757  rplpwr  16764  sqgcd  16768  expgcd  16769  rpmulgcd2  16863  rpdvds  16867  coprmproddvdslem  16869  isprm5  16915  divgcdodd  16918  dvdszzq  16929  divnumden  16956  crth  16987  phimullem  16988  modprm0  17015  modprmn0modprm0  17017  coprimeprodsq2  17019  pythagtriplem19  17043  pockthlem  17115  prmunb  17124  prmreclem3  17128  prmreclem6  17131  ramub  17223  ramz  17235  kerf1ghm  19493  pmtrprfv  19700  pmtrprfv3  19701  mndodcong  19789  odngen  19824  pgpfi  19852  sylow2blem3  19869  lsmless1  19907  lsmless2  19908  lsmless12  19909  lsmmod2  19923  pj1id  19946  odadd2  20096  gexexlem  20099  ablfacrplem  20314  ablfacrp  20315  ablfac1b  20319  ablfac1eu  20322  pgpfac1lem2  20324  ogrpaddlt  20385  elrhmunit  20793  rrgnz  20989  ornglmullt  21159  orngrmullt  21160  lsmssspx  21396  lspsncv0  21457  qsidomlem1  21669  ssdifidlprm  21675  znunit  21902  uvcvvcl2  22127  uvcvv1  22128  uvcvv0  22129  coe1subfv  22618  coe1fzgsumdlem  22654  scmate  22858  mdetunilem2  22961  matunitlindflem2  23028  pmatcoe1fsupp  23052  mat2pmatlin  23086  decpmatmullem  23122  pmatcollpw1lem1  23125  pmatcollpw1lem2  23126  pm2mpghm  23167  chpscmat  23193  chp0mat  23197  chpidmat  23198  cpmadugsumlemB  23225  cpmadugsumlemC  23226  cpmadugsumlemF  23227  clsndisj  23426  neiptopnei  23483  rnelfm  24305  fmfnfmlem2  24307  fmfnfm  24310  flimss1  24325  isfcf  24386  cnextfun  24416  cnextfvval  24417  cnextf  24418  cnextcn  24419  cnextfres1  24420  ustuqtop1  24593  utopsnneiplem  24599  xblss2ps  24753  xblss2  24754  stdbdxmet  24867  metcnpi3  24898  metustexhalf  24908  nmoi  25080  nmoi2  25082  nmoco  25089  blcvx  25150  icccmplem2  25176  icccmplem3  25177  reconnlem2  25180  xrge0gsumle  25186  metds0  25203  metdstri  25204  metdseq0  25207  lebnumlem3  25317  nmoleub2lem  25468  bcthlem5  25682  csschl  25730  minveclem2  25780  minveclem3b  25782  minveclem4  25786  minveclem6  25788  icombl  25918  cncombf  26012  mbflimsup  26020  itg2monolem1  26104  itg2cnlem1  26115  itg2cnlem2  26116  bddmulibl  26192  ellimc2  26230  cpnord  26288  cpnres  26290  dvmulbr  26292  dvcobr  26299  dvlipcn  26347  dvlip2  26348  dvivthlem1  26361  lhop1lem  26366  lhop1  26367  dvfsumlem2  26380  itgsubstlem  26401  deg1add  26454  deg1sublt  26461  ply1remlem  26516  plyeq0lem  26562  taylthlem2  26734  ulmdvlem3  26762  abelthlem7  26798  pilem2  26812  pilem3  26813  pige3ALT  26881  logccv  27024  cxpaddlelem  27112  cvxcl  27345  fsumharmonic  27372  ftalem5  27437  mpodvdsmulf1o  27554  dvdsmulf1o  27556  bposlem1  27644  lgsqr  27711  lgsquad2lem2  27745  2lgsoddprmlem1  27768  2sqlem8a  27785  2sqlem8  27786  dchrmusum2  27854  dchrvmasumiflem1  27861  dchrisum0flblem1  27868  dchrisum0lem1b  27875  pntlem3  27969  flt4lem4  28012  noetasuplem4  28126  noetainflem4  28130  noetalem1  28131  divmulswd  28613  divsclwd  28615  uzsind  28824  tgdim01  29003  axsegcon  29538  ax5seglem1  29539  ax5seglem2  29540  axlowdimlem6  29558  axeuclidlem  29573  axcontlem7  29581  axcontlem9  29583  axcontlem10  29584  nbupgr  29958  nbumgrvtx  29960  cusgrsize2inds  30067  upgriswlk  30254  2pthnloop  30350  numclwwlk2lem1  31010  frgrreg  31028  nmoub3i  31408  ubthlem3  31507  minvecolem2  31510  minvecolem4  31515  minvecolem5  31516  minvecolem6  31517  htthlem  31552  pjpjpre  32054  chscllem1  32272  chscllem2  32273  chscllem3  32274  cnlnadjlem2  32703  leopnmid  32773  tpssad  33210  br8d  33277  splfv3  33592  symgcom2  33721  cyc3genpmlem  33788  archirngz  33826  elrgspnlem1  33879  erld2  33903  rlocf1  33911  subrdom  33922  ricdomn1  33926  dvdsruasso  34024  unitpidl1  34058  mxidlirredi  34080  dflringlem2  34111  1arithidomlem2  34152  1arithidom  34153  1arithufdlem3  34162  ply1gsumz  34214  mplidomlem  34242  esplymhp  34283  esplyfvaln  34289  vietadeg1  34293  lssdimle  34323  dimkerim  34342  fedgmullem2  34345  fedgmul  34346  assalactf1o  34350  fldextrspundglemul  34394  fldextrspundgdvds  34396  minplyirred  34426  irredminply  34431  algextdeglem2  34433  rtelextdg2lem  34441  constrext2chnlem  34465  constrresqrtcl  34492  2sqr3minply  34495  cos9thpiminplylem2  34498  cos9thpiminply  34503  qqhval2lem  34696  qqhnm  34705  qqhucn  34707  esumcst  34778  esumpcvgval  34793  measunl  34932  dya2iocbrsiga  34990  dya2icobrsiga  34991  omssubadd  35015  inelcarsg  35026  carsgclctunlem2  35034  sibfof  35055  sitgaddlemb  35063  oddpwdc  35069  eulerpartlemgc  35077  bayesth  35154  ftc2re  35310  breprexplemc  35344  tgoldbachgt  35375  dfk12  36025  dfk22  36026  dfk32  36027  erdszelem8  36143  2goelgoanfmla1  36369  br8  36712  totbndbnd  38926  prdsbnd  38930  rrncmslem  38969  rrntotbnd  38973  isdrngo2  39095  lsatcmp  40263  lcvexchlem2  40295  lcvexchlem3  40296  ncvr1  40532  cvrletrN  40533  cvrnbtwn3  40536  cvrnrefN  40542  cvrcmp  40543  0ltat  40551  atnle0  40569  atlen0  40570  cvlcvr1  40599  cvrval3  40673  atle  40696  athgt  40716  1cvratex  40733  ps-2  40738  ps-2b  40742  llnnleat  40773  2atneat  40775  llnle  40778  atcvrlln  40780  llncmp  40782  2llnmat  40784  2at0mat0  40785  2atm  40787  ps-2c  40788  lplnle  40800  lplnnle2at  40801  llncvrlpln2  40817  llncvrlpln  40818  2lplnmN  40819  2llnmj  40820  2atmat  40821  lplncmp  40822  lplnexllnN  40824  2llnm2N  40828  2llnm4  40830  lvolnle3at  40842  4atlem3a  40857  4atlem3b  40858  4atlem10  40866  4atlem11  40869  4atlem12  40872  lplncvrlvol2  40875  lplncvrlvol  40876  lvolcmp  40877  2lplnm2N  40881  2lplnmj  40882  dalempjsen  40913  dalemcea  40920  dalem2  40921  dalemdea  40922  dalem9  40932  dalem16  40939  dalemcjden  40952  dalem21  40954  dalem23  40956  dalem39  40971  dalem54  40986  dalem60  40992  cdlemb  41054  elpadd2at  41066  paddasslem4  41083  paddasslem7  41086  paddasslem15  41094  paddasslem16  41095  pmodlem1  41106  pmodlem2  41107  llnexchb2  41129  pclfinclN  41210  osumcllem9N  41224  pmapojoinN  41228  pexmidN  41229  pl42lem1N  41239  lhp0lt  41263  lhpexle1  41268  lhpexle2lem  41269  lhpexle3lem  41271  lhprelat3N  41300  ltrnid  41395  trlval3  41447  arglem1N  41450  cdlemc5  41455  cdleme3b  41489  cdleme3c  41490  cdleme3h  41495  cdleme7e  41507  cdleme7ga  41508  cdleme20l1  41580  cdleme20l2  41581  cdleme20l  41582  cdleme22b  41601  cdlemefrs29clN  41659  cdlemefrs32fva  41660  cdlemeg46fvcl  41766  cdlemeg46c  41773  cdlemeg46fvaw  41776  cdlemeg46req  41789  cdleme48fgv  41798  cdlemf1  41821  cdlemg1cex  41848  cdlemg2dN  41850  cdlemg2ce  41852  cdlemg12e  41907  cdlemg35  41973  cdlemh  42077  tendocan  42084  cdlemk28-3  42168  tendoex  42235  dih1  42546  dihmeetlem9N  42575  dihlspsnssN  42592  dihlspsnat  42593  lcfrlem23  42825  renegneg  43667  fsuppind  43822  3cubes  43904  mzpsubst  43963  rencldnfi  44032  irrapx1  44039  pellexlem3  44042  pellexlem5  44044  infmrgelbi  44089  pellqrex  44090  pellfundge  44093  rmspecfund  44120  congtr  44176  acongeq  44194  jm2.20nn  44208  jm2.25lem1  44209  jm2.26  44213  expdiophlem1  44232  hbtlem2  44329  cantnftermord  44525  suprleubrd  45369  suprlubrd  45371  suprnmpt  46404  wessf1ornlem  46415  mpct  46430  upbdrech  46536  ssfiunibd  46540  uzfissfz  46553  xleadd2d  46554  suprltrp  46555  xleadd1d  46556  suprleubrnmpt  46647  iccintsng  46750  limcrecl  46856  fnlimfvre  46899  dvmulcncf  47150  dvdivcncf  47152  dvbdfbdioolem1  47153  ioodvbdlimc1lem2  47157  ioodvbdlimc2lem  47159  stoweidlem1  47226  stoweidlem20  47245  stoweidlem24  47249  stoweidlem34  47259  stoweidlem45  47270  stoweidlem60  47285  fourierdlem20  47352  fourierdlem31  47363  fourierdlem38  47370  fourierdlem64  47395  fourierdlem79  47410  fourierdlem94  47425  fourierdlem113  47444  fouriersw  47456  fouriercn  47457  sge0isum  47652  hoicvr  47773  ovnsubaddlem2  47796  hoidmv1lelem1  47816  hoidmv1lelem3  47818  hoidmvlelem1  47820  hoidmvlelem4  47823  smflimlem2  47997  2timesltsq  48663  fmtnof1  48835  lighneallem2  48906  uspgrlim  49305  upgrwlkupwlk  49453  lincresunit3  49808  elbigolo1  49884