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 206  df-an 396

This theorem is referenced by:  anass  468  anabss3  672  biadanid  820  rspc4v  3623  f1elima  7255  fnfvof  7681  frxp3  8132  oecl  8533  oaass  8557  oen0  8582  oeworde  8589  omabs  8647  oiiniseg  9525  cardinfima  10089  fpwwe2lem11  10633  ltmul12a  12068  eluzp1m1  12846  lbzbi  12918  qreccl  12951  xrlttr  13117  elfzodifsumelfzo  13696  quoremnn0  13819  incexc2  15782  mertens  15830  ndvdsadd  16352  nn0seqcvgd  16506  isprm3  16619  isprm7  16644  pcval  16778  prdsval  17402  evlfcl  18179  frgpup1  19687  frgpup3lem  19689  ghmcmn  19743  gsumval3  19819  gsumzoppg  19856  ablfaclem2  20000  gsumdixp  20210  frlmgsum  21637  psrass1lemOLD  21804  psrass1lem  21807  psrass1  21837  m2cpminvid2  22581  pmatcollpw2lem  22603  chcoeffeqlem  22711  neissex  22955  neiptopnei  22960  dissnlocfin  23357  tx1stc  23478  kqreglem1  23569  xpstopnlem1  23637  alexsublem  23872  metuel2  24398  icoopnst  24787  iocopnst  24788  volcn  25459  mbflimsup  25519  mbflim  25521  itg1addlem4  25552  itg1addlem4OLD  25553  itg1addlem5  25554  itg1climres  25568  limcflf  25734  dvcobr  25801  dvcobrOLD  25802  dvcnvlem  25832  dvfsumge  25880  mdegmullem  25938  plyeq0lem  26066  plypf1  26068  mtestbdd  26260  mbfulm  26261  fsumdvdscom  27036  muinv  27044  logfaclbnd  27074  logexprlim  27077  dchrinv  27113  lgsval3  27167  2sqmo  27289  rpvmasum2  27364  dchrisum0lem1  27368  dchrisum0  27372  selberg  27400  selberg3lem1  27409  selberg34r  27423  pntsval2  27428  nosupbnd1lem5  27564  noinfbnd1lem5  27579  nocvxminlem  27629  oldbday  27746  iscgrglt  28237  ercgrg  28240  legso  28322  oppperpex  28476  hpgerlem  28488  trgcopyeu  28529  dfcgra2  28553  inaghl  28568  colinearalg  28640  axeuclid  28693  axcontlem2  28695  axcontlem7  28700  wlkiswwlksupgr2  29603  grpoidinvlem4  30232  ipblnfi  30580  shmodsi  31114  eighmorth  31689  kbass5  31845  kbass6  31846  dmdmd  32025  atom1d  32078  mdsymlem2  32129  mdsymlem3  32130  mdsymlem4  32131  mdsymlem5  32132  fmptco1f1o  32329  2ndresdju  32346  fnpreimac  32368  fsumiunle  32505  s3f1  32583  swrdf1  32590  dfmgc2lem  32635  dfmgc2  32636  pwrssmgc  32640  mgcf1o  32643  gsummpt2co  32671  tocyccntz  32774  cycpmconjs  32786  urpropd  32849  isdrng4  32864  suborng  32902  eqgvscpbl  32934  dvdsruasso  32962  nsgmgclem  32994  nsgmgc  32995  nsgqusf1olem2  32997  nsgqusf1olem3  32998  ghmquskerlem3  33003  lmhmqusker  33006  intlidl  33008  rhmpreimaidl  33009  rhmquskerlem  33015  elrspunidl  33018  elrspunsn  33019  idlinsubrg  33021  rhmimaidl  33022  drngidl  33023  prmidl2  33031  idlmulssprm  33032  isprmidlc  33038  rhmpreimaprmidl  33042  qsidomlem1  33043  qsidomlem2  33044  mxidlprm  33058  mxidlirredi  33059  ssmxidllem  33061  opprlidlabs  33071  qsdrngi  33081  r1plmhm  33149  r1pquslmic  33150  ply1degltdimlem  33189  ply1degltdim  33190  lindsun  33192  lbsdiflsp0  33193  fedgmullem1  33196  fedgmul  33198  extdg1id  33224  evls1maplmhm  33243  minplyirred  33253  algextdeglem8  33263  zart0  33351  pstmxmet  33369  ordtconnlem1  33396  esumiun  33584  dya2iocnei  33773  omssubadd  33791  actfunsnf1o  34107  fsum2dsub  34110  reprsuc  34118  reprinfz1  34125  reprpmtf1o  34129  breprexplema  34133  circlemeth  34143  hgt750lemb  34159  cusgr3cyclex  34618  resconn  34728  pibt2  36789  uncf  36961  unccur  36965  fin2so  36969  matunitlindflem1  36978  poimirlem6  36988  poimirlem7  36989  poimirlem25  37007  poimirlem28  37010  poimirlem31  37013  poimirlem32  37014  broucube  37016  ismblfin  37023  mbfposadd  37029  itg2gt0cn  37037  ftc1anclem7  37061  ftc1anc  37063  cover2  37077  indexa  37095  filbcmb  37102  seqpo  37109  incsequz  37110  isbnd2  37145  ghomco  37253  unichnidl  37393  isfldidl  37430  dihvalc  40598  dihvalb  40602  uzindd  41339  aks4d1p8  41449  evlselv  41652  fsuppind  41655  radcnvrat  43587  reximddv3  44353  rexabslelem  44638  rexlimddv2  45049  dvnprodlem2  45173  etransclem46  45506  lubeldm2  47801  glbeldm2  47802  aacllem  48060