Theorem anasss 470

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 423	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 422	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anass  472  anabss3  674  f1elima  6999  fnfvof  7403  oecl  8145  oaass  8170  oen0  8195  oeworde  8202  omabs  8257  oiiniseg  8981  cardinfima  9508  fpwwe2lem12  10052  ltmul12a  11485  eluzp1m1  12256  lbzbi  12324  qreccl  12356  xrlttr  12521  elfzodifsumelfzo  13098  quoremnn0  13219  incexc2  15185  mertens  15234  ndvdsadd  15751  nn0seqcvgd  15904  isprm3  16017  isprm7  16042  pcval  16171  prdsval  16720  evlfcl  17464  frgpup1  18893  frgpup3lem  18895  ghmcmn  18945  gsumval3  19020  gsumzoppg  19057  ablfaclem2  19201  gsumdixp  19355  frlmgsum  20461  psrass1lem  20615  psrass1  20643  m2cpminvid2  21360  pmatcollpw2lem  21382  chcoeffeqlem  21490  neissex  21732  neiptopnei  21737  dissnlocfin  22134  tx1stc  22255  kqreglem1  22346  xpstopnlem1  22414  alexsublem  22649  metuel2  23172  icoopnst  23544  iocopnst  23545  volcn  24210  mbflimsup  24270  mbflim  24272  itg1addlem4  24303  itg1addlem5  24304  itg1climres  24318  limcflf  24484  dvcobr  24549  dvcnvlem  24579  dvfsumge  24625  mdegmullem  24679  plyeq0lem  24807  plypf1  24809  mtestbdd  25000  mbfulm  25001  fsumdvdscom  25770  muinv  25778  logfaclbnd  25806  logexprlim  25809  dchrinv  25845  lgsval3  25899  2sqmo  26021  rpvmasum2  26096  dchrisum0lem1  26100  dchrisum0  26104  selberg  26132  selberg3lem1  26141  selberg34r  26155  pntsval2  26160  iscgrglt  26308  ercgrg  26311  legso  26393  oppperpex  26547  hpgerlem  26559  trgcopyeu  26600  dfcgra2  26624  inaghl  26639  colinearalg  26704  axeuclid  26757  axcontlem2  26759  axcontlem7  26764  wlkiswwlksupgr2  27663  grpoidinvlem4  28290  ipblnfi  28638  shmodsi  29172  eighmorth  29747  kbass5  29903  kbass6  29904  dmdmd  30083  atom1d  30136  mdsymlem2  30187  mdsymlem3  30188  mdsymlem4  30189  mdsymlem5  30190  biadanid  30236  fmptco1f1o  30392  2ndresdju  30411  fnpreimac  30434  fsumiunle  30571  s3f1  30649  swrdf1  30656  dfmgc2lem  30703  dfmgc2  30704  pwrssmgc  30706  gsummpt2co  30733  tocyccntz  30836  cycpmconjs  30848  suborng  30939  eqgvscpbl  30970  intlidl  31010  rhmpreimaidl  31011  elrspunidl  31014  idlinsubrg  31016  rhmimaidl  31017  prmidl2  31024  idlmulssprm  31025  isprmidlc  31031  rhmpreimaprmidl  31035  qsidomlem1  31036  qsidomlem2  31037  mxidlprm  31048  ssmxidllem  31049  lindsun  31109  lbsdiflsp0  31110  fedgmullem1  31113  fedgmul  31115  extdg1id  31141  zart0  31232  pstmxmet  31250  ordtconnlem1  31277  esumiun  31463  dya2iocnei  31650  omssubadd  31668  actfunsnf1o  31985  fsum2dsub  31988  reprsuc  31996  reprinfz1  32003  reprpmtf1o  32007  breprexplema  32011  circlemeth  32021  hgt750lemb  32037  cusgr3cyclex  32496  resconn  32606  nosupbnd1lem5  33325  nocvxminlem  33360  pibt2  34834  uncf  35036  unccur  35040  fin2so  35044  matunitlindflem1  35053  poimirlem6  35063  poimirlem7  35064  poimirlem25  35082  poimirlem28  35085  poimirlem31  35088  poimirlem32  35089  broucube  35091  ismblfin  35098  mbfposadd  35104  itg2gt0cn  35112  ftc1anclem7  35136  ftc1anc  35138  cover2  35152  indexa  35171  filbcmb  35178  seqpo  35185  incsequz  35186  isbnd2  35221  ghomco  35329  unichnidl  35469  isfldidl  35506  dihvalc  38529  dihvalb  38533  uzindd  39264  fsuppind  39456  radcnvrat  41018  reximddv3  41788  rexabslelem  42055  rexlimddv2  42465  dvnprodlem2  42589  etransclem46  42922  aacllem  45329