Theorem anasss 466

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
anasss.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
anasss	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem anasss

Step	Hyp	Ref	Expression
1		anasss.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	exp31 419	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 418	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  anass  468  anabss3  676  biadanid  823  reximddv3  3154  rspc4v  3584  f1elima  7218  fnfvof  7648  frxp3  8101  oecl  8472  oaass  8496  oen0  8522  oeworde  8529  omabs  8587  oiiniseg  9448  cardinfima  10019  fpwwe2lem11  10564  ltmul12a  12011  eluzp1m1  12814  lbzbi  12886  qreccl  12919  xrlttr  13091  elfzodifsumelfzo  13686  quoremnn0  13815  incexc2  15803  mertens  15851  ndvdsadd  16379  nn0seqcvgd  16539  isprm3  16652  isprm7  16678  pcval  16815  prdsval  17418  evlfcl  18188  chnso  18590  ghmqusnsg  19257  ghmquskerlem3  19261  frgpup1  19750  frgpup3lem  19752  ghmcmn  19806  gsumval3  19882  gsumzoppg  19919  ablfaclem2  20063  gsumdixp  20298  suborng  20853  rhmpreimaidl  21275  rhmqusnsg  21283  frlmgsum  21752  psrass1lem  21912  psrass1  21942  psdmul  22132  evls1maplmhm  22342  m2cpminvid2  22720  pmatcollpw2lem  22742  chcoeffeqlem  22850  neissex  23092  neiptopnei  23097  dissnlocfin  23494  tx1stc  23615  kqreglem1  23706  xpstopnlem1  23774  alexsublem  24009  metuel2  24530  icoopnst  24906  iocopnst  24907  volcn  25573  mbflimsup  25633  mbflim  25635  itg1addlem4  25666  itg1addlem5  25667  itg1climres  25681  limcflf  25848  dvcobr  25913  dvcnvlem  25943  dvfsumge  25989  mdegmullem  26043  plyeq0lem  26175  plypf1  26177  mtestbdd  26370  mbfulm  26371  fsumdvdscom  27148  muinv  27156  logfaclbnd  27185  logexprlim  27188  dchrinv  27224  lgsval3  27278  2sqmo  27400  rpvmasum2  27475  dchrisum0lem1  27479  dchrisum0  27483  selberg  27511  selberg3lem1  27520  selberg34r  27534  pntsval2  27539  nosupbnd1lem5  27676  noinfbnd1lem5  27691  nocvxminlem  27746  oldbday  27893  peano5uzs  28396  iscgrglt  28582  ercgrg  28585  legso  28667  oppperpex  28821  hpgerlem  28833  trgcopyeu  28874  dfcgra2  28898  inaghl  28913  colinearalg  28979  axeuclid  29032  axcontlem2  29034  axcontlem7  29039  wlkiswwlksupgr2  29945  grpoidinvlem4  30578  ipblnfi  30926  shmodsi  31460  eighmorth  32035  kbass5  32191  kbass6  32192  dmdmd  32371  atom1d  32424  mdsymlem2  32475  mdsymlem3  32476  mdsymlem4  32477  mdsymlem5  32478  fmptco1f1o  32706  2ndresdju  32722  fnpreimac  32743  fsumiunle  32902  s3f1  33007  swrdf1  33016  dfmgc2lem  33055  dfmgc2  33056  pwrssmgc  33060  mgcf1o  33063  mndlrinvb  33085  mndlactf1  33086  mndractf1  33088  gsummpt2co  33109  gsumwrd2dccatlem  33138  tocyccntz  33205  cycpmconjs  33217  conjga  33231  fxpsubrg  33235  urpropd  33292  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem2  33309  elrgspnsubrun  33310  erler  33326  rlocaddval  33329  rlocmulval  33330  rlocf1  33334  domnprodn0  33336  domnprodeq0  33337  rrgsubm  33345  subrdom  33346  isdrng4  33356  eqgvscpbl  33410  dvdsruasso  33445  nsgmgclem  33471  nsgmgc  33472  nsgqusf1olem2  33474  nsgqusf1olem3  33475  lmhmqusker  33477  intlidl  33480  rhmquskerlem  33485  elrspunidl  33488  elrspunsn  33489  idlinsubrg  33491  rhmimaidl  33492  drngidl  33493  prmidl2  33501  idlmulssprm  33502  isprmidlc  33507  rhmpreimaprmidl  33511  qsidomlem1  33512  qsidomlem2  33513  ssdifidllem  33516  ssdifidlprm  33518  mxidlprm  33530  mxidlirredi  33531  ssmxidllem  33533  opprlidlabs  33545  qsdrngi  33555  rsprprmprmidl  33582  rsprprmprmidlb  33583  rprmirred  33591  rprmirredb  33592  rprmdvdsprod  33594  1arithidom  33597  1arithufdlem3  33606  1arithufdlem4  33607  deg1prod  33643  r1plmhm  33670  r1pquslmic  33671  extvfvcl  33680  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  psrgsum  33692  psrmonprod  33696  esplyfval1  33717  esplyfvaln  33718  vieta  33724  ply1degltdimlem  33766  ply1degltdim  33767  lindsun  33769  lbsdiflsp0  33770  fedgmullem1  33773  fedgmul  33775  lactlmhm  33778  assalactf1o  33779  extdg1id  33810  fldextrspunlsplem  33817  fldextrspunlsp  33818  extdgfialglem2  33837  extdgfialg  33838  minplyirred  33855  algextdeglem8  33868  constrextdg2lem  33892  constrextdg2  33893  constrfiss  33895  constrsdrg  33919  cos9thpiminplylem2  33927  zart0  34023  pstmxmet  34041  ordtconnlem1  34068  esumiun  34238  dya2iocnei  34426  omssubadd  34444  actfunsnf1o  34748  fsum2dsub  34751  reprsuc  34759  reprinfz1  34766  reprpmtf1o  34770  breprexplema  34774  circlemeth  34784  hgt750lemb  34800  cusgr3cyclex  35318  resconn  35428  pibt2  37733  uncf  37920  unccur  37924  fin2so  37928  matunitlindflem1  37937  poimirlem6  37947  poimirlem7  37948  poimirlem25  37966  poimirlem28  37969  poimirlem31  37972  poimirlem32  37973  broucube  37975  ismblfin  37982  mbfposadd  37988  itg2gt0cn  37996  ftc1anclem7  38020  ftc1anc  38022  cover2  38036  indexa  38054  filbcmb  38061  seqpo  38068  incsequz  38069  isbnd2  38104  ghomco  38212  unichnidl  38352  isfldidl  38389  dihvalc  41679  dihvalb  41683  uzindd  42417  aks4d1p8  42526  evlselv  43020  fsuppind  43023  radcnvrat  44741  rexabslelem  45846  rexlimddv2  46251  dvnprodlem2  46375  etransclem46  46708  isgrtri  48419  grlimgrtri  48479  lubeldm2  49431  glbeldm2  49432  thincciso2  49930  aacllem  50276