Theorem syl31anc 1371

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  syl32anc  1376  stoic4b  1784  elovmpt3rab1  7520  smo11  8179  omeulem2  8390  oeeui  8409  oaabs2  8453  omabs  8455  omxpenlem  8829  map2xp  8899  mapdom2  8900  fsuppsssupp  9105  cantnflt  9391  cnfcom  9419  mapdjuen  9920  pwsdompw  9944  ackbij1lem5  9964  cofsmo  10009  fin1a2lem4  10143  ltmul12a  11814  lt2msq1  11842  ledivp1  11860  lemul1ad  11897  lemul2ad  11898  suprubd  11920  supaddc  11925  supadd  11926  supmul1  11927  supmul  11930  rpnnen1lem3  12701  rpnnen1lem5  12703  lediv2ad  12776  xaddge0  12974  xadddi  13011  xadddi2  13013  supicc  13215  supicclub  13217  difelfznle  13352  flval3  13516  expcan  13868  ltexp2  13869  ltexp2r  13872  expubnd  13876  ltexp2rd  13944  ltexp2d  13949  leexp2d  13950  expcand  13951  hashmap  14131  swrds1  14360  ccatswrd  14362  pfxfv  14376  swrdccatin1  14419  pfxccatin12lem3  14426  cshwidxmod  14497  wrdl3s3  14658  o1fsum  15506  mertenslem1  15577  eftlub  15799  rpnnen2lem4  15907  ruclem12  15931  dvdsadd  15992  3dvds  16021  divalgmod  16096  bitsmod  16124  bitsinv1lem  16129  bezoutlem4  16231  gcdzeq  16243  rplpwr  16248  sqgcd  16251  rpmulgcd2  16342  rpdvds  16346  coprmproddvdslem  16348  isprm5  16393  divgcdodd  16396  divnumden  16433  crth  16460  phimullem  16461  modprm0  16487  modprmn0modprm0  16489  coprimeprodsq2  16491  pythagtriplem19  16515  pockthlem  16587  prmunb  16596  prmreclem3  16600  prmreclem6  16603  ramub  16695  ramz  16707  pmtrprfv  19042  pmtrprfv3  19043  mndodcong  19131  odngen  19163  pgpfi  19191  sylow2blem3  19208  lsmless1  19246  lsmless2  19247  lsmless12  19248  lsmmod2  19263  pj1id  19286  odadd2  19431  gexexlem  19434  ablfacrplem  19649  ablfacrp  19650  ablfac1b  19654  ablfac1eu  19657  pgpfac1lem2  19659  kerf1ghm  19968  lsmssspx  20331  lspsncv0  20389  znunit  20752  uvcvvcl2  20976  uvcvv1  20977  uvcvv0  20978  coe1subfv  21418  coe1fzgsumdlem  21453  scmate  21640  mdetunilem2  21743  pmatcoe1fsupp  21831  mat2pmatlin  21865  decpmatmullem  21901  pmatcollpw1lem1  21904  pmatcollpw1lem2  21905  pm2mpghm  21946  chpscmat  21972  chp0mat  21976  chpidmat  21977  cpmadugsumlemB  22004  cpmadugsumlemC  22005  cpmadugsumlemF  22006  clsndisj  22207  neiptopnei  22264  rnelfm  23085  fmfnfmlem2  23087  fmfnfm  23090  flimss1  23105  isfcf  23166  cnextfun  23196  cnextfvval  23197  cnextf  23198  cnextcn  23199  cnextfres1  23200  ustuqtop1  23374  utopsnneiplem  23380  xblss2ps  23535  xblss2  23536  stdbdxmet  23652  metcnpi3  23683  metustexhalf  23693  nmoi  23873  nmoi2  23875  nmoco  23882  blcvx  23942  icccmplem2  23967  icccmplem3  23968  reconnlem2  23971  xrge0gsumle  23977  metds0  23994  metdstri  23995  metdseq0  23998  lebnumlem3  24107  nmoleub2lem  24258  bcthlem5  24473  csschl  24521  minveclem2  24571  minveclem3b  24573  minveclem4  24577  minveclem6  24579  icombl  24709  cncombf  24803  mbflimsup  24811  itg2monolem1  24896  itg2cnlem1  24907  itg2cnlem2  24908  bddmulibl  24984  ellimc2  25022  cpnord  25080  cpnres  25082  dvmulbr  25084  dvcobr  25091  dvlipcn  25139  dvlip2  25140  dvivthlem1  25153  lhop1lem  25158  lhop1  25159  dvfsumlem2  25172  itgsubstlem  25193  deg1add  25249  deg1sublt  25256  ply1remlem  25308  plyeq0lem  25352  taylthlem2  25514  ulmdvlem3  25542  abelthlem7  25578  pilem2  25592  pilem3  25593  pige3ALT  25657  logccv  25799  cxpaddlelem  25885  cvxcl  26115  fsumharmonic  26142  ftalem5  26207  dvdsmulf1o  26324  bposlem1  26413  lgsqr  26480  lgsquad2lem2  26514  2lgsoddprmlem1  26537  2sqlem8a  26554  2sqlem8  26555  dchrmusum2  26623  dchrvmasumiflem1  26630  dchrisum0flblem1  26637  dchrisum0lem1b  26644  pntlem3  26738  tgdim01  26849  axsegcon  27276  ax5seglem1  27277  ax5seglem2  27278  axlowdimlem6  27296  axeuclidlem  27311  axcontlem7  27319  axcontlem9  27321  axcontlem10  27322  nbupgr  27692  nbumgrvtx  27694  cusgrsize2inds  27801  upgriswlk  27988  2pthnloop  28078  numclwwlk2lem1  28719  frgrreg  28737  nmoub3i  29114  ubthlem3  29213  minvecolem2  29216  minvecolem4  29221  minvecolem5  29222  minvecolem6  29223  htthlem  29258  pjpjpre  29760  chscllem1  29978  chscllem2  29979  chscllem3  29980  cnlnadjlem2  30409  leopnmid  30479  br8d  30929  dvdszzq  31108  swrdf1  31207  splfv3  31209  ogrpaddlt  31322  symgcom2  31332  cyc3genpmlem  31397  archirngz  31422  ornglmullt  31485  orngrmullt  31486  elrhmunit  31498  elrspunidl  31585  qsidomlem1  31607  lssdimle  31670  dimkerim  31687  fedgmullem2  31690  fedgmul  31691  qqhval2lem  31910  qqhnm  31919  qqhucn  31921  esumcst  32010  esumpcvgval  32025  measunl  32163  dya2iocbrsiga  32221  dya2icobrsiga  32222  omssubadd  32246  inelcarsg  32257  carsgclctunlem2  32265  sibfof  32286  sitgaddlemb  32294  oddpwdc  32300  eulerpartlemgc  32308  bayesth  32385  ftc2re  32557  breprexplemc  32591  tgoldbachgt  32622  erdszelem8  33139  2goelgoanfmla1  33365  br8  33702  noetasuplem4  33918  noetainflem4  33922  noetalem1  33923  matunitlindflem2  35753  totbndbnd  35926  prdsbnd  35930  rrncmslem  35969  rrntotbnd  35973  isdrngo2  36095  lsatcmp  36996  lcvexchlem2  37028  lcvexchlem3  37029  ncvr1  37265  cvrletrN  37266  cvrnbtwn3  37269  cvrnrefN  37275  cvrcmp  37276  0ltat  37284  atnle0  37302  atlen0  37303  cvlcvr1  37332  cvrval3  37406  atle  37429  athgt  37449  1cvratex  37466  ps-2  37471  ps-2b  37475  llnnleat  37506  2atneat  37508  llnle  37511  atcvrlln  37513  llncmp  37515  2llnmat  37517  2at0mat0  37518  2atm  37520  ps-2c  37521  lplnle  37533  lplnnle2at  37534  llncvrlpln2  37550  llncvrlpln  37551  2lplnmN  37552  2llnmj  37553  2atmat  37554  lplncmp  37555  lplnexllnN  37557  2llnm2N  37561  2llnm4  37563  lvolnle3at  37575  4atlem3a  37590  4atlem3b  37591  4atlem10  37599  4atlem11  37602  4atlem12  37605  lplncvrlvol2  37608  lplncvrlvol  37609  lvolcmp  37610  2lplnm2N  37614  2lplnmj  37615  dalempjsen  37646  dalemcea  37653  dalem2  37654  dalemdea  37655  dalem9  37665  dalem16  37672  dalemcjden  37685  dalem21  37687  dalem23  37689  dalem39  37704  dalem54  37719  dalem60  37725  cdlemb  37787  elpadd2at  37799  paddasslem4  37816  paddasslem7  37819  paddasslem15  37827  paddasslem16  37828  pmodlem1  37839  pmodlem2  37840  llnexchb2  37862  pclfinclN  37943  osumcllem9N  37957  pmapojoinN  37961  pexmidN  37962  pl42lem1N  37972  lhp0lt  37996  lhpexle1  38001  lhpexle2lem  38002  lhpexle3lem  38004  lhprelat3N  38033  ltrnid  38128  trlval3  38180  arglem1N  38183  cdlemc5  38188  cdleme3b  38222  cdleme3c  38223  cdleme3h  38228  cdleme7e  38240  cdleme7ga  38241  cdleme20l1  38313  cdleme20l2  38314  cdleme20l  38315  cdleme22b  38334  cdlemefrs29clN  38392  cdlemefrs32fva  38393  cdlemeg46fvcl  38499  cdlemeg46c  38506  cdlemeg46fvaw  38509  cdlemeg46req  38522  cdleme48fgv  38531  cdlemf1  38554  cdlemg1cex  38581  cdlemg2dN  38583  cdlemg2ce  38585  cdlemg12e  38640  cdlemg35  38706  cdlemh  38810  tendocan  38817  cdlemk28-3  38901  tendoex  38968  dih1  39279  dihmeetlem9N  39308  dihlspsnssN  39325  dihlspsnat  39326  lcfrlem23  39558  3rspcedvdw  40161  fsuppind  40259  expgcd  40314  renegneg  40374  flt4lem4  40466  3cubes  40492  mzpsubst  40550  rencldnfi  40623  irrapx1  40630  pellexlem3  40633  pellexlem5  40635  infmrgelbi  40680  pellqrex  40681  pellfundge  40684  rmspecfund  40711  congtr  40767  acongeq  40785  jm2.20nn  40799  jm2.25lem1  40800  jm2.26  40804  expdiophlem1  40823  hbtlem2  40929  suprleubrd  41730  suprlubrd  41732  suprnmpt  42663  wessf1ornlem  42675  mpct  42694  upbdrech  42798  ssfiunibd  42802  uzfissfz  42819  xleadd2d  42820  suprltrp  42821  xleadd1d  42822  suprleubrnmpt  42916  iccintsng  43015  limcrecl  43124  fnlimfvre  43169  dvmulcncf  43420  dvdivcncf  43422  dvbdfbdioolem1  43423  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  stoweidlem1  43496  stoweidlem20  43515  stoweidlem24  43519  stoweidlem34  43529  stoweidlem45  43540  stoweidlem60  43555  fourierdlem20  43622  fourierdlem31  43633  fourierdlem38  43640  fourierdlem64  43665  fourierdlem79  43680  fourierdlem94  43695  fourierdlem113  43714  fouriersw  43726  fouriercn  43727  sge0isum  43919  hoicvr  44040  ovnsubaddlem2  44063  hoidmv1lelem1  44083  hoidmv1lelem3  44085  hoidmvlelem1  44087  hoidmvlelem4  44090  smflimlem2  44258  fmtnof1  44939  lighneallem2  45010  upgrwlkupwlk  45254  lincresunit3  45774  elbigolo1  45855  eenglngeehlnm  46037