Theorem syl31anc 1369

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  syl32anc  1374  stoic4b  1779  elovmpt3rab1  7405  smo11  8001  omeulem2  8209  oeeui  8228  oaabs2  8272  omabs  8274  omxpenlem  8618  map2xp  8687  mapdom2  8688  fsuppsssupp  8849  cantnflt  9135  cnfcom  9163  mapdjuen  9606  pwsdompw  9626  ackbij1lem5  9646  cofsmo  9691  fin1a2lem4  9825  ltmul12a  11496  lt2msq1  11524  ledivp1  11542  lemul1ad  11579  lemul2ad  11580  suprubd  11603  supaddc  11608  supadd  11609  supmul1  11610  supmul  11613  rpnnen1lem3  12379  rpnnen1lem5  12381  lediv2ad  12454  xaddge0  12652  xadddi  12689  xadddi2  12691  supicc  12887  supicclub  12889  difelfznle  13022  flval3  13186  expcan  13534  ltexp2  13535  ltexp2r  13538  expubnd  13542  ltexp2rd  13610  ltexp2d  13615  leexp2d  13616  expcand  13617  hashmap  13797  swrds1  14028  ccatswrd  14030  pfxfv  14044  swrdccatin1  14087  pfxccatin12lem3  14094  cshwidxmod  14165  wrdl3s3  14326  o1fsum  15168  mertenslem1  15240  eftlub  15462  rpnnen2lem4  15570  ruclem12  15594  dvdsadd  15652  3dvds  15680  divalgmod  15757  bitsmod  15785  bitsinv1lem  15790  bezoutlem4  15890  gcdzeq  15902  rplpwr  15907  sqgcd  15909  rpmulgcd2  16000  rpdvds  16004  coprmproddvdslem  16006  isprm5  16051  divgcdodd  16054  divnumden  16088  crth  16115  phimullem  16116  modprm0  16142  modprmn0modprm0  16144  coprimeprodsq2  16146  pythagtriplem19  16170  pockthlem  16241  prmunb  16250  prmreclem3  16254  prmreclem6  16257  ramub  16349  ramz  16361  pmtrprfv  18581  pmtrprfv3  18582  mndodcong  18670  odngen  18702  pgpfi  18730  sylow2blem3  18747  lsmless1  18785  lsmless2  18786  lsmless12  18787  lsmmod2  18802  pj1id  18825  odadd2  18969  gexexlem  18972  ablfacrplem  19187  ablfacrp  19188  ablfac1b  19192  ablfac1eu  19195  pgpfac1lem2  19197  kerf1ghm  19497  kerf1hrmOLD  19498  lsmssspx  19860  lspsncv0  19918  coe1subfv  20434  coe1fzgsumdlem  20469  znunit  20710  uvcvvcl2  20932  uvcvv1  20933  uvcvv0  20934  scmate  21119  mdetunilem2  21222  pmatcoe1fsupp  21309  mat2pmatlin  21343  decpmatmullem  21379  pmatcollpw1lem1  21382  pmatcollpw1lem2  21383  pm2mpghm  21424  chpscmat  21450  chp0mat  21454  chpidmat  21455  cpmadugsumlemB  21482  cpmadugsumlemC  21483  cpmadugsumlemF  21484  clsndisj  21683  neiptopnei  21740  rnelfm  22561  fmfnfmlem2  22563  fmfnfm  22566  flimss1  22581  isfcf  22642  cnextfun  22672  cnextfvval  22673  cnextf  22674  cnextcn  22675  cnextfres1  22676  ustuqtop1  22850  utopsnneiplem  22856  xblss2ps  23011  xblss2  23012  stdbdxmet  23125  metcnpi3  23156  metustexhalf  23166  nmoi  23337  nmoi2  23339  nmoco  23346  blcvx  23406  icccmplem2  23431  icccmplem3  23432  reconnlem2  23435  xrge0gsumle  23441  metds0  23458  metdstri  23459  metdseq0  23462  lebnumlem3  23567  nmoleub2lem  23718  bcthlem5  23931  csschl  23979  minveclem2  24029  minveclem3b  24031  minveclem4  24035  minveclem6  24037  icombl  24165  cncombf  24259  mbflimsup  24267  itg2monolem1  24351  itg2cnlem1  24362  itg2cnlem2  24363  bddmulibl  24439  ellimc2  24475  cpnord  24532  cpnres  24534  dvmulbr  24536  dvcobr  24543  dvlipcn  24591  dvlip2  24592  dvivthlem1  24605  lhop1lem  24610  lhop1  24611  dvfsumlem2  24624  itgsubstlem  24645  deg1add  24697  deg1sublt  24704  ply1remlem  24756  plyeq0lem  24800  taylthlem2  24962  ulmdvlem3  24990  abelthlem7  25026  pilem2  25040  pilem3  25041  pige3ALT  25105  logccv  25246  cxpaddlelem  25332  cvxcl  25562  fsumharmonic  25589  ftalem5  25654  dvdsmulf1o  25771  bposlem1  25860  lgsqr  25927  lgsquad2lem2  25961  2lgsoddprmlem1  25984  2sqlem8a  26001  2sqlem8  26002  dchrmusum2  26070  dchrvmasumiflem1  26077  dchrisum0flblem1  26084  dchrisum0lem1b  26091  pntlem3  26185  tgdim01  26293  axsegcon  26713  ax5seglem1  26714  ax5seglem2  26715  axlowdimlem6  26733  axeuclidlem  26748  axcontlem7  26756  axcontlem9  26758  axcontlem10  26759  nbupgr  27126  nbumgrvtx  27128  cusgrsize2inds  27235  upgriswlk  27422  2pthnloop  27512  numclwwlk2lem1  28155  frgrreg  28173  nmoub3i  28550  ubthlem3  28649  minvecolem2  28652  minvecolem4  28657  minvecolem5  28658  minvecolem6  28659  htthlem  28694  pjpjpre  29196  chscllem1  29414  chscllem2  29415  chscllem3  29416  cnlnadjlem2  29845  leopnmid  29915  br8d  30361  dvdszzq  30531  swrdf1  30630  splfv3  30632  ogrpaddlt  30718  symgcom2  30728  cyc3genpmlem  30793  archirngz  30818  ornglmullt  30880  orngrmullt  30881  elrhmunit  30893  qsidomlem1  30965  lssdimle  31006  dimkerim  31023  fedgmullem2  31026  fedgmul  31027  qqhval2lem  31222  qqhnm  31231  qqhucn  31233  esumcst  31322  esumpcvgval  31337  measunl  31475  dya2iocbrsiga  31533  dya2icobrsiga  31534  omssubadd  31558  inelcarsg  31569  carsgclctunlem2  31577  sibfof  31598  sitgaddlemb  31606  oddpwdc  31612  eulerpartlemgc  31620  bayesth  31697  ftc2re  31869  breprexplemc  31903  tgoldbachgt  31934  erdszelem8  32445  2goelgoanfmla1  32671  br8  32992  noetalem3  33219  noetalem5  33221  matunitlindflem2  34904  totbndbnd  35082  prdsbnd  35086  rrncmslem  35125  rrntotbnd  35129  isdrngo2  35251  lsatcmp  36154  lcvexchlem2  36186  lcvexchlem3  36187  ncvr1  36423  cvrletrN  36424  cvrnbtwn3  36427  cvrnrefN  36433  cvrcmp  36434  0ltat  36442  atnle0  36460  atlen0  36461  cvlcvr1  36490  cvrval3  36564  atle  36587  athgt  36607  1cvratex  36624  ps-2  36629  ps-2b  36633  llnnleat  36664  2atneat  36666  llnle  36669  atcvrlln  36671  llncmp  36673  2llnmat  36675  2at0mat0  36676  2atm  36678  ps-2c  36679  lplnle  36691  lplnnle2at  36692  llncvrlpln2  36708  llncvrlpln  36709  2lplnmN  36710  2llnmj  36711  2atmat  36712  lplncmp  36713  lplnexllnN  36715  2llnm2N  36719  2llnm4  36721  lvolnle3at  36733  4atlem3a  36748  4atlem3b  36749  4atlem10  36757  4atlem11  36760  4atlem12  36763  lplncvrlvol2  36766  lplncvrlvol  36767  lvolcmp  36768  2lplnm2N  36772  2lplnmj  36773  dalempjsen  36804  dalemcea  36811  dalem2  36812  dalemdea  36813  dalem9  36823  dalem16  36830  dalemcjden  36843  dalem21  36845  dalem23  36847  dalem39  36862  dalem54  36877  dalem60  36883  cdlemb  36945  elpadd2at  36957  paddasslem4  36974  paddasslem7  36977  paddasslem15  36985  paddasslem16  36986  pmodlem1  36997  pmodlem2  36998  llnexchb2  37020  pclfinclN  37101  osumcllem9N  37115  pmapojoinN  37119  pexmidN  37120  pl42lem1N  37130  lhp0lt  37154  lhpexle1  37159  lhpexle2lem  37160  lhpexle3lem  37162  lhprelat3N  37191  ltrnid  37286  trlval3  37338  arglem1N  37341  cdlemc5  37346  cdleme3b  37380  cdleme3c  37381  cdleme3h  37386  cdleme7e  37398  cdleme7ga  37399  cdleme20l1  37471  cdleme20l2  37472  cdleme20l  37473  cdleme22b  37492  cdlemefrs29clN  37550  cdlemefrs32fva  37551  cdlemeg46fvcl  37657  cdlemeg46c  37664  cdlemeg46fvaw  37667  cdlemeg46req  37680  cdleme48fgv  37689  cdlemf1  37712  cdlemg1cex  37739  cdlemg2dN  37741  cdlemg2ce  37743  cdlemg12e  37798  cdlemg35  37864  cdlemh  37968  tendocan  37975  cdlemk28-3  38059  tendoex  38126  dih1  38437  dihmeetlem9N  38466  dihlspsnssN  38483  dihlspsnat  38484  lcfrlem23  38716  expgcd  39203  renegneg  39261  3cubes  39307  mzpsubst  39365  rencldnfi  39438  irrapx1  39445  pellexlem3  39448  pellexlem5  39450  infmrgelbi  39495  pellqrex  39496  pellfundge  39499  rmspecfund  39526  congtr  39582  acongeq  39600  jm2.20nn  39614  jm2.25lem1  39615  jm2.26  39619  expdiophlem1  39638  hbtlem2  39744  suprleubrd  40537  suprlubrd  40540  suprnmpt  41450  wessf1ornlem  41465  mpct  41484  upbdrech  41592  ssfiunibd  41596  uzfissfz  41614  xleadd2d  41615  suprltrp  41616  xleadd1d  41617  suprleubrnmpt  41716  iccintsng  41819  limcrecl  41930  fnlimfvre  41975  dvmulcncf  42230  dvdivcncf  42232  dvbdfbdioolem1  42233  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  stoweidlem1  42306  stoweidlem20  42325  stoweidlem24  42329  stoweidlem34  42339  stoweidlem45  42350  stoweidlem60  42365  fourierdlem20  42432  fourierdlem31  42443  fourierdlem38  42450  fourierdlem64  42475  fourierdlem79  42490  fourierdlem94  42505  fourierdlem113  42524  fouriersw  42536  fouriercn  42537  sge0isum  42729  hoicvr  42850  ovnsubaddlem2  42873  hoidmv1lelem1  42893  hoidmv1lelem3  42895  hoidmvlelem1  42897  hoidmvlelem4  42900  smflimlem2  43068  fmtnof1  43717  lighneallem2  43791  upgrwlkupwlk  44035  lincresunit3  44556  elbigolo1  44637  eenglngeehlnm  44746