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  3155  rspc4v  3585  f1elima  7211  fnfvof  7641  frxp3  8094  oecl  8465  oaass  8489  oen0  8515  oeworde  8522  omabs  8580  oiiniseg  9441  cardinfima  10010  fpwwe2lem11  10555  ltmul12a  12002  eluzp1m1  12805  lbzbi  12877  qreccl  12910  xrlttr  13082  elfzodifsumelfzo  13677  quoremnn0  13806  incexc2  15794  mertens  15842  ndvdsadd  16370  nn0seqcvgd  16530  isprm3  16643  isprm7  16669  pcval  16806  prdsval  17409  evlfcl  18179  chnso  18581  ghmqusnsg  19248  ghmquskerlem3  19252  frgpup1  19741  frgpup3lem  19743  ghmcmn  19797  gsumval3  19873  gsumzoppg  19910  ablfaclem2  20054  gsumdixp  20289  suborng  20844  rhmpreimaidl  21267  rhmqusnsg  21275  frlmgsum  21762  psrass1lem  21922  psrass1  21952  psdmul  22142  evls1maplmhm  22352  m2cpminvid2  22730  pmatcollpw2lem  22752  chcoeffeqlem  22860  neissex  23102  neiptopnei  23107  dissnlocfin  23504  tx1stc  23625  kqreglem1  23716  xpstopnlem1  23784  alexsublem  24019  metuel2  24540  icoopnst  24916  iocopnst  24917  volcn  25583  mbflimsup  25643  mbflim  25645  itg1addlem4  25676  itg1addlem5  25677  itg1climres  25691  limcflf  25858  dvcobr  25923  dvcnvlem  25953  dvfsumge  25999  mdegmullem  26053  plyeq0lem  26185  plypf1  26187  mtestbdd  26383  mbfulm  26384  fsumdvdscom  27162  muinv  27170  logfaclbnd  27199  logexprlim  27202  dchrinv  27238  lgsval3  27292  2sqmo  27414  rpvmasum2  27489  dchrisum0lem1  27493  dchrisum0  27497  selberg  27525  selberg3lem1  27534  selberg34r  27548  pntsval2  27553  nosupbnd1lem5  27690  noinfbnd1lem5  27705  nocvxminlem  27760  oldbday  27907  peano5uzs  28410  iscgrglt  28596  ercgrg  28599  legso  28681  oppperpex  28835  hpgerlem  28847  trgcopyeu  28888  dfcgra2  28912  inaghl  28927  colinearalg  28993  axeuclid  29046  axcontlem2  29048  axcontlem7  29053  wlkiswwlksupgr2  29960  grpoidinvlem4  30593  ipblnfi  30941  shmodsi  31475  eighmorth  32050  kbass5  32206  kbass6  32207  dmdmd  32386  atom1d  32439  mdsymlem2  32490  mdsymlem3  32491  mdsymlem4  32492  mdsymlem5  32493  fmptco1f1o  32721  2ndresdju  32737  fnpreimac  32758  fsumiunle  32917  s3f1  33022  swrdf1  33031  dfmgc2lem  33070  dfmgc2  33071  pwrssmgc  33075  mgcf1o  33078  mndlrinvb  33100  mndlactf1  33101  mndractf1  33103  gsummpt2co  33124  gsumwrd2dccatlem  33153  tocyccntz  33220  cycpmconjs  33232  conjga  33246  fxpsubrg  33250  urpropd  33307  elrgspnlem2  33319  elrgspnlem4  33321  elrgspnsubrunlem2  33324  elrgspnsubrun  33325  erler  33341  rlocaddval  33344  rlocmulval  33345  rlocf1  33349  domnprodn0  33351  domnprodeq0  33352  rrgsubm  33360  subrdom  33361  isdrng4  33371  eqgvscpbl  33425  dvdsruasso  33460  nsgmgclem  33486  nsgmgc  33487  nsgqusf1olem2  33489  nsgqusf1olem3  33490  lmhmqusker  33492  intlidl  33495  rhmquskerlem  33500  elrspunidl  33503  elrspunsn  33504  idlinsubrg  33506  rhmimaidl  33507  drngidl  33508  prmidl2  33516  idlmulssprm  33517  isprmidlc  33522  rhmpreimaprmidl  33526  qsidomlem1  33527  qsidomlem2  33528  ssdifidllem  33531  ssdifidlprm  33533  mxidlprm  33545  mxidlirredi  33546  ssmxidllem  33548  opprlidlabs  33560  qsdrngi  33570  rsprprmprmidl  33597  rsprprmprmidlb  33598  rprmirred  33606  rprmirredb  33607  rprmdvdsprod  33609  1arithidom  33612  1arithufdlem3  33621  1arithufdlem4  33622  deg1prod  33658  r1plmhm  33685  r1pquslmic  33686  extvfvcl  33695  mplvrpmga  33704  mplvrpmmhm  33705  mplvrpmrhm  33706  psrgsum  33707  psrmonprod  33711  esplyfval1  33732  esplyfvaln  33733  vieta  33739  ply1degltdimlem  33782  ply1degltdim  33783  lindsun  33785  lbsdiflsp0  33786  fedgmullem1  33789  fedgmul  33791  lactlmhm  33794  assalactf1o  33795  extdg1id  33826  fldextrspunlsplem  33833  fldextrspunlsp  33834  extdgfialglem2  33853  extdgfialg  33854  minplyirred  33871  algextdeglem8  33884  constrextdg2lem  33908  constrextdg2  33909  constrfiss  33911  constrsdrg  33935  cos9thpiminplylem2  33943  zart0  34039  pstmxmet  34057  ordtconnlem1  34084  esumiun  34254  dya2iocnei  34442  omssubadd  34460  actfunsnf1o  34764  fsum2dsub  34767  reprsuc  34775  reprinfz1  34782  reprpmtf1o  34786  breprexplema  34790  circlemeth  34800  hgt750lemb  34816  cusgr3cyclex  35334  resconn  35444  pibt2  37747  uncf  37934  unccur  37938  fin2so  37942  matunitlindflem1  37951  poimirlem6  37961  poimirlem7  37962  poimirlem25  37980  poimirlem28  37983  poimirlem31  37986  poimirlem32  37987  broucube  37989  ismblfin  37996  mbfposadd  38002  itg2gt0cn  38010  ftc1anclem7  38034  ftc1anc  38036  cover2  38050  indexa  38068  filbcmb  38075  seqpo  38082  incsequz  38083  isbnd2  38118  ghomco  38226  unichnidl  38366  isfldidl  38403  dihvalc  41693  dihvalb  41697  uzindd  42431  aks4d1p8  42540  evlselv  43034  fsuppind  43037  radcnvrat  44759  rexabslelem  45864  rexlimddv2  46269  dvnprodlem2  46393  etransclem46  46726  isgrtri  48431  grlimgrtri  48491  lubeldm2  49443  glbeldm2  49444  thincciso2  49942  aacllem  50288