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  675  biadanid  823  reximddv3  3169  rspc4v  3641  f1elima  7282  fnfvof  7713  frxp3  8174  oecl  8573  oaass  8597  oen0  8622  oeworde  8629  omabs  8687  oiiniseg  9570  cardinfima  10134  fpwwe2lem11  10678  ltmul12a  12120  eluzp1m1  12901  lbzbi  12975  qreccl  13008  xrlttr  13178  elfzodifsumelfzo  13766  quoremnn0  13892  incexc2  15870  mertens  15918  ndvdsadd  16443  nn0seqcvgd  16603  isprm3  16716  isprm7  16741  pcval  16877  prdsval  17501  evlfcl  18278  ghmqusnsg  19312  ghmquskerlem3  19316  frgpup1  19807  frgpup3lem  19809  ghmcmn  19863  gsumval3  19939  gsumzoppg  19976  ablfaclem2  20120  gsumdixp  20332  rhmpreimaidl  21304  rhmqusnsg  21312  frlmgsum  21809  psrass1lem  21969  psrass1  22001  psdmul  22187  evls1maplmhm  22396  m2cpminvid2  22776  pmatcollpw2lem  22798  chcoeffeqlem  22906  neissex  23150  neiptopnei  23155  dissnlocfin  23552  tx1stc  23673  kqreglem1  23764  xpstopnlem1  23832  alexsublem  24067  metuel2  24593  icoopnst  24982  iocopnst  24983  volcn  25654  mbflimsup  25714  mbflim  25716  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  itg1climres  25763  limcflf  25930  dvcobr  25997  dvcobrOLD  25998  dvcnvlem  26028  dvfsumge  26076  mdegmullem  26131  plyeq0lem  26263  plypf1  26265  mtestbdd  26462  mbfulm  26463  fsumdvdscom  27242  muinv  27250  logfaclbnd  27280  logexprlim  27283  dchrinv  27319  lgsval3  27373  2sqmo  27495  rpvmasum2  27570  dchrisum0lem1  27574  dchrisum0  27578  selberg  27606  selberg3lem1  27615  selberg34r  27629  pntsval2  27634  nosupbnd1lem5  27771  noinfbnd1lem5  27786  nocvxminlem  27836  oldbday  27953  peano5uzs  28404  iscgrglt  28536  ercgrg  28539  legso  28621  oppperpex  28775  hpgerlem  28787  trgcopyeu  28828  dfcgra2  28852  inaghl  28867  colinearalg  28939  axeuclid  28992  axcontlem2  28994  axcontlem7  28999  wlkiswwlksupgr2  29906  grpoidinvlem4  30535  ipblnfi  30883  shmodsi  31417  eighmorth  31992  kbass5  32148  kbass6  32149  dmdmd  32328  atom1d  32381  mdsymlem2  32432  mdsymlem3  32433  mdsymlem4  32434  mdsymlem5  32435  fmptco1f1o  32649  2ndresdju  32665  fnpreimac  32687  fsumiunle  32835  s3f1  32915  swrdf1  32925  dfmgc2lem  32969  dfmgc2  32970  pwrssmgc  32974  mgcf1o  32977  chnso  32987  mndlrinvb  33012  mndlactf1  33013  mndractf1  33015  gsummpt2co  33033  gsumwrd2dccatlem  33051  tocyccntz  33146  cycpmconjs  33158  urpropd  33221  elrgspnlem2  33232  elrgspnlem4  33234  erler  33251  rlocaddval  33254  rlocmulval  33255  rlocf1  33259  domnprodn0  33261  rrgsubm  33267  subrdom  33268  isdrng4  33278  suborng  33324  eqgvscpbl  33357  dvdsruasso  33392  nsgmgclem  33418  nsgmgc  33419  nsgqusf1olem2  33421  nsgqusf1olem3  33422  lmhmqusker  33424  intlidl  33427  rhmquskerlem  33432  elrspunidl  33435  elrspunsn  33436  idlinsubrg  33438  rhmimaidl  33439  drngidl  33440  prmidl2  33448  idlmulssprm  33449  isprmidlc  33454  rhmpreimaprmidl  33458  qsidomlem1  33459  qsidomlem2  33460  ssdifidllem  33463  ssdifidlprm  33465  mxidlprm  33477  mxidlirredi  33478  ssmxidllem  33480  opprlidlabs  33492  qsdrngi  33502  rsprprmprmidl  33529  rsprprmprmidlb  33530  rprmirred  33538  rprmirredb  33539  rprmdvdsprod  33541  1arithidom  33544  1arithufdlem3  33553  1arithufdlem4  33554  r1plmhm  33609  r1pquslmic  33610  ply1degltdimlem  33649  ply1degltdim  33650  lindsun  33652  lbsdiflsp0  33653  fedgmullem1  33656  fedgmul  33658  lactlmhm  33661  assalactf1o  33662  extdg1id  33690  minplyirred  33718  algextdeglem8  33729  zart0  33839  pstmxmet  33857  ordtconnlem1  33884  esumiun  34074  dya2iocnei  34263  omssubadd  34281  actfunsnf1o  34597  fsum2dsub  34600  reprsuc  34608  reprinfz1  34615  reprpmtf1o  34619  breprexplema  34623  circlemeth  34633  hgt750lemb  34649  cusgr3cyclex  35120  resconn  35230  pibt2  37399  uncf  37585  unccur  37589  fin2so  37593  matunitlindflem1  37602  poimirlem6  37612  poimirlem7  37613  poimirlem25  37631  poimirlem28  37634  poimirlem31  37637  poimirlem32  37638  broucube  37640  ismblfin  37647  mbfposadd  37653  itg2gt0cn  37661  ftc1anclem7  37685  ftc1anc  37687  cover2  37701  indexa  37719  filbcmb  37726  seqpo  37733  incsequz  37734  isbnd2  37769  ghomco  37877  unichnidl  38017  isfldidl  38054  dihvalc  41215  dihvalb  41219  uzindd  41958  aks4d1p8  42068  evlselv  42573  fsuppind  42576  radcnvrat  44309  rexabslelem  45367  rexlimddv2  45778  dvnprodlem2  45902  etransclem46  46235  isgrtri  47847  grlimgrtri  47898  lubeldm2  48752  glbeldm2  48753  aacllem  49031