Theorem syl31anc 1375

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

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

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 1088

This theorem is referenced by:  syl32anc  1380  stoic4b  1778  3rspcedvdw  3606  elovmpt3rab1  7649  smo11  8333  omeulem2  8547  oeeui  8566  oaabs2  8613  omabs  8615  omxpenlem  9042  map2xp  9111  mapdom2  9112  fsuppsssupp  9332  cantnflt  9625  cnfcom  9653  mapdjuen  10134  pwsdompw  10156  ackbij1lem5  10176  cofsmo  10222  fin1a2lem4  10356  ltmul12a  12038  lt2msq1  12067  ledivp1  12085  lemul1ad  12122  lemul2ad  12123  suprubd  12145  supaddc  12150  supadd  12151  supmul1  12152  supmul  12155  rpnnen1lem3  12938  rpnnen1lem5  12940  lediv2ad  13017  xaddge0  13218  xadddi  13255  xadddi2  13257  supicc  13462  supicclub  13464  difelfznle  13603  flval3  13777  expcan  14134  ltexp2  14135  ltexp2r  14138  expubnd  14143  ltexp2rd  14213  ltexp2d  14216  leexp2d  14217  expcand  14218  hashmap  14400  swrds1  14631  ccatswrd  14633  pfxfv  14647  swrdccatin1  14690  pfxccatin12lem3  14697  cshwidxmod  14768  wrdl3s3  14928  o1fsum  15779  mertenslem1  15850  eftlub  16077  rpnnen2lem4  16185  ruclem12  16209  dvdsadd  16272  3dvds  16301  divalgmod  16376  bitsmod  16406  bitsinv1lem  16411  bezoutlem4  16512  gcdzeq  16522  rplpwr  16528  sqgcd  16532  expgcd  16533  rpmulgcd2  16626  rpdvds  16630  coprmproddvdslem  16632  isprm5  16677  divgcdodd  16680  dvdszzq  16691  divnumden  16718  crth  16748  phimullem  16749  modprm0  16776  modprmn0modprm0  16778  coprimeprodsq2  16780  pythagtriplem19  16804  pockthlem  16876  prmunb  16885  prmreclem3  16889  prmreclem6  16892  ramub  16984  ramz  16996  kerf1ghm  19179  pmtrprfv  19383  pmtrprfv3  19384  mndodcong  19472  odngen  19507  pgpfi  19535  sylow2blem3  19552  lsmless1  19590  lsmless2  19591  lsmless12  19592  lsmmod2  19606  pj1id  19629  odadd2  19779  gexexlem  19782  ablfacrplem  19997  ablfacrp  19998  ablfac1b  20002  ablfac1eu  20005  pgpfac1lem2  20007  elrhmunit  20419  rrgnz  20613  lsmssspx  20995  lspsncv0  21056  znunit  21473  uvcvvcl2  21697  uvcvv1  21698  uvcvv0  21699  coe1subfv  22152  coe1fzgsumdlem  22190  scmate  22397  mdetunilem2  22500  pmatcoe1fsupp  22588  mat2pmatlin  22622  decpmatmullem  22658  pmatcollpw1lem1  22661  pmatcollpw1lem2  22662  pm2mpghm  22703  chpscmat  22729  chp0mat  22733  chpidmat  22734  cpmadugsumlemB  22761  cpmadugsumlemC  22762  cpmadugsumlemF  22763  clsndisj  22962  neiptopnei  23019  rnelfm  23840  fmfnfmlem2  23842  fmfnfm  23845  flimss1  23860  isfcf  23921  cnextfun  23951  cnextfvval  23952  cnextf  23953  cnextcn  23954  cnextfres1  23955  ustuqtop1  24129  utopsnneiplem  24135  xblss2ps  24289  xblss2  24290  stdbdxmet  24403  metcnpi3  24434  metustexhalf  24444  nmoi  24616  nmoi2  24618  nmoco  24625  blcvx  24686  icccmplem2  24712  icccmplem3  24713  reconnlem2  24716  xrge0gsumle  24722  metds0  24739  metdstri  24740  metdseq0  24743  lebnumlem3  24862  nmoleub2lem  25014  bcthlem5  25228  csschl  25276  minveclem2  25326  minveclem3b  25328  minveclem4  25332  minveclem6  25334  icombl  25465  cncombf  25559  mbflimsup  25567  itg2monolem1  25651  itg2cnlem1  25662  itg2cnlem2  25663  bddmulibl  25740  ellimc2  25778  cpnord  25837  cpnres  25839  dvmulbr  25841  dvmulbrOLD  25842  dvcobr  25849  dvcobrOLD  25850  dvlipcn  25899  dvlip2  25900  dvivthlem1  25913  lhop1lem  25918  lhop1  25919  dvfsumlem2  25933  dvfsumlem2OLD  25934  itgsubstlem  25955  deg1add  26008  deg1sublt  26015  ply1remlem  26070  plyeq0lem  26115  taylthlem2  26282  taylthlem2OLD  26283  ulmdvlem3  26311  abelthlem7  26348  pilem2  26362  pilem3  26363  pige3ALT  26429  logccv  26572  cxpaddlelem  26661  cvxcl  26895  fsumharmonic  26922  ftalem5  26987  mpodvdsmulf1o  27104  dvdsmulf1o  27106  bposlem1  27195  lgsqr  27262  lgsquad2lem2  27296  2lgsoddprmlem1  27319  2sqlem8a  27336  2sqlem8  27337  dchrmusum2  27405  dchrvmasumiflem1  27412  dchrisum0flblem1  27419  dchrisum0lem1b  27426  pntlem3  27520  noetasuplem4  27648  noetainflem4  27652  noetalem1  27653  divsmulwd  28097  divsclwd  28099  uzsind  28293  tgdim01  28434  axsegcon  28854  ax5seglem1  28855  ax5seglem2  28856  axlowdimlem6  28874  axeuclidlem  28889  axcontlem7  28897  axcontlem9  28899  axcontlem10  28900  nbupgr  29271  nbumgrvtx  29273  cusgrsize2inds  29381  upgriswlk  29569  2pthnloop  29661  numclwwlk2lem1  30305  frgrreg  30323  nmoub3i  30702  ubthlem3  30801  minvecolem2  30804  minvecolem4  30809  minvecolem5  30810  minvecolem6  30811  htthlem  30846  pjpjpre  31348  chscllem1  31566  chscllem2  31567  chscllem3  31568  cnlnadjlem2  31997  leopnmid  32067  tpssad  32468  br8d  32538  swrdf1  32878  splfv3  32880  ogrpaddlt  33031  symgcom2  33041  cyc3genpmlem  33108  archirngz  33143  elrgspnlem1  33193  rlocf1  33224  subrdom  33235  ornglmullt  33285  orngrmullt  33286  dvdsruasso  33356  unitpidl1  33395  elrspunidl  33399  qsidomlem1  33423  ssdifidlprm  33429  mxidlirredi  33442  1arithidomlem2  33507  1arithidom  33508  1arithufdlem3  33517  ply1gsumz  33564  lssdimle  33603  dimkerim  33623  fedgmullem2  33626  fedgmul  33627  assalactf1o  33631  fldextrspundglemul  33674  fldextrspundgdvds  33676  minplyirred  33701  irredminply  33706  algextdeglem2  33708  rtelextdg2lem  33716  constrext2chnlem  33740  constrresqrtcl  33767  2sqr3minply  33770  cos9thpiminplylem2  33773  cos9thpiminply  33778  qqhval2lem  33971  qqhnm  33980  qqhucn  33982  esumcst  34053  esumpcvgval  34068  measunl  34206  dya2iocbrsiga  34266  dya2icobrsiga  34267  omssubadd  34291  inelcarsg  34302  carsgclctunlem2  34310  sibfof  34331  sitgaddlemb  34339  oddpwdc  34345  eulerpartlemgc  34353  bayesth  34430  ftc2re  34589  breprexplemc  34623  tgoldbachgt  34654  erdszelem8  35185  2goelgoanfmla1  35411  br8  35743  matunitlindflem2  37611  totbndbnd  37783  prdsbnd  37787  rrncmslem  37826  rrntotbnd  37830  isdrngo2  37952  lsatcmp  38996  lcvexchlem2  39028  lcvexchlem3  39029  ncvr1  39265  cvrletrN  39266  cvrnbtwn3  39269  cvrnrefN  39275  cvrcmp  39276  0ltat  39284  atnle0  39302  atlen0  39303  cvlcvr1  39332  cvrval3  39407  atle  39430  athgt  39450  1cvratex  39467  ps-2  39472  ps-2b  39476  llnnleat  39507  2atneat  39509  llnle  39512  atcvrlln  39514  llncmp  39516  2llnmat  39518  2at0mat0  39519  2atm  39521  ps-2c  39522  lplnle  39534  lplnnle2at  39535  llncvrlpln2  39551  llncvrlpln  39552  2lplnmN  39553  2llnmj  39554  2atmat  39555  lplncmp  39556  lplnexllnN  39558  2llnm2N  39562  2llnm4  39564  lvolnle3at  39576  4atlem3a  39591  4atlem3b  39592  4atlem10  39600  4atlem11  39603  4atlem12  39606  lplncvrlvol2  39609  lplncvrlvol  39610  lvolcmp  39611  2lplnm2N  39615  2lplnmj  39616  dalempjsen  39647  dalemcea  39654  dalem2  39655  dalemdea  39656  dalem9  39666  dalem16  39673  dalemcjden  39686  dalem21  39688  dalem23  39690  dalem39  39705  dalem54  39720  dalem60  39726  cdlemb  39788  elpadd2at  39800  paddasslem4  39817  paddasslem7  39820  paddasslem15  39828  paddasslem16  39829  pmodlem1  39840  pmodlem2  39841  llnexchb2  39863  pclfinclN  39944  osumcllem9N  39958  pmapojoinN  39962  pexmidN  39963  pl42lem1N  39973  lhp0lt  39997  lhpexle1  40002  lhpexle2lem  40003  lhpexle3lem  40005  lhprelat3N  40034  ltrnid  40129  trlval3  40181  arglem1N  40184  cdlemc5  40189  cdleme3b  40223  cdleme3c  40224  cdleme3h  40229  cdleme7e  40241  cdleme7ga  40242  cdleme20l1  40314  cdleme20l2  40315  cdleme20l  40316  cdleme22b  40335  cdlemefrs29clN  40393  cdlemefrs32fva  40394  cdlemeg46fvcl  40500  cdlemeg46c  40507  cdlemeg46fvaw  40510  cdlemeg46req  40523  cdleme48fgv  40532  cdlemf1  40555  cdlemg1cex  40582  cdlemg2dN  40584  cdlemg2ce  40586  cdlemg12e  40641  cdlemg35  40707  cdlemh  40811  tendocan  40818  cdlemk28-3  40902  tendoex  40969  dih1  41280  dihmeetlem9N  41309  dihlspsnssN  41326  dihlspsnat  41327  lcfrlem23  41559  renegneg  42400  fsuppind  42578  flt4lem4  42637  3cubes  42678  mzpsubst  42736  rencldnfi  42809  irrapx1  42816  pellexlem3  42819  pellexlem5  42821  infmrgelbi  42866  pellqrex  42867  pellfundge  42870  rmspecfund  42897  congtr  42954  acongeq  42972  jm2.20nn  42986  jm2.25lem1  42987  jm2.26  42991  expdiophlem1  43010  hbtlem2  43113  cantnftermord  43309  suprleubrd  44155  suprlubrd  44157  suprnmpt  45168  wessf1ornlem  45179  mpct  45195  upbdrech  45303  ssfiunibd  45307  uzfissfz  45322  xleadd2d  45323  suprltrp  45324  xleadd1d  45325  suprleubrnmpt  45418  iccintsng  45521  limcrecl  45627  fnlimfvre  45672  dvmulcncf  45923  dvdivcncf  45925  dvbdfbdioolem1  45926  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem1  45999  stoweidlem20  46018  stoweidlem24  46022  stoweidlem34  46032  stoweidlem45  46043  stoweidlem60  46058  fourierdlem20  46125  fourierdlem31  46136  fourierdlem38  46143  fourierdlem64  46168  fourierdlem79  46183  fourierdlem94  46198  fourierdlem113  46217  fouriersw  46229  fouriercn  46230  sge0isum  46425  hoicvr  46546  ovnsubaddlem2  46569  hoidmv1lelem1  46589  hoidmv1lelem3  46591  hoidmvlelem1  46593  hoidmvlelem4  46596  smflimlem2  46770  fmtnof1  47536  lighneallem2  47607  uspgrlim  47991  upgrwlkupwlk  48128  lincresunit3  48470  elbigolo1  48546  eenglngeehlnm  48728