Theorem anasss 471

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  anass  473  anabss3  687  biadanid  834  3anasss  1378  reximddv3  3188  rspc4v  3610  f1elima  7259  fnfvof  7689  frxp3  8143  oecl  8518  oaass  8542  oen0  8568  oeworde  8575  omabs  8633  oiiniseg  9491  cardinfima  10077  fpwwe2lem11  10622  ltmul12a  12067  eluzp1m1  12884  lbzbi  12956  qreccl  12989  xrlttr  13161  elfzodifsumelfzo  13756  quoremnn0  13885  incexc2  15888  mertens  15936  ndvdsadd  16464  nn0seqcvgd  16624  isprm3  16737  isprm7  16763  pcval  16900  prdsval  17504  evlfcl  18274  chnso  18676  ghmqusnsg  19348  ghmquskerlem3  19352  frgpup1  19841  frgpup3lem  19843  ghmcmn  19897  gsumval3  19973  gsumzoppg  20010  ablfaclem2  20154  gsumdixp  20396  suborng  20953  rhmpreimaidl  21383  rhmqusnsg  21392  prmidl2  21433  idlmulssprm  21434  isprmidlc  21439  rhmpreimaprmidl  21444  qsidomlem1  21445  qsidomlem2  21446  ssdifidllem  21449  ssdifidlprm  21451  prmidlsubm  21452  frlmgsum  21887  psrass1lem  22048  psrass1  22078  psdmul  22294  evls1maplmhm  22502  m2cpminvid2  22877  pmatcollpw2lem  22899  chcoeffeqlem  23007  neissex  23249  neiptopnei  23254  dissnlocfin  23651  tx1stc  23772  kqreglem1  23863  xpstopnlem1  23931  alexsublem  24166  metuel2  24687  icoopnst  25063  iocopnst  25064  volcn  25730  mbflimsup  25790  mbflim  25792  itg1addlem4  25823  itg1addlem5  25824  itg1climres  25838  limcflf  26005  dvcobr  26070  dvcnvlem  26100  dvfsumge  26146  mdegmullem  26200  plyeq0lem  26332  plypf1  26334  mtestbdd  26530  mbfulm  26531  fsumdvdscom  27311  muinv  27319  logfaclbnd  27348  logexprlim  27351  dchrinv  27387  lgsval3  27441  2sqmo  27563  rpvmasum2  27638  dchrisum0lem1  27642  dchrisum0  27646  selberg  27674  selberg3lem1  27683  selberg34r  27697  pntsval2  27702  nosupbnd1lem5  27838  noinfbnd1lem5  27853  nocvxminlem  27909  oldbday  28056  peano5uzs  28559  iscgrglt  28745  ercgrg  28748  legso  28830  tglinesseq  28871  tglnpt3  28885  tglnpt4  28886  oppperpex  28989  hpgerlem  29002  isplng  29014  plngrotlem3  29025  plng3p  29033  trgcopyeu  29070  dfcgra2  29094  ragcgra  29099  inaghl  29113  prlnghpg  29147  prlngex  29150  prlngmolem1  29151  prlngmolem2  29152  colinearalg  29197  axeuclid  29250  axcontlem2  29252  axcontlem7  29257  wlkiswwlksupgr2  30163  grpoidinvlem4  30796  ipblnfi  31144  shmodsi  31678  eighmorth  32253  kbass5  32409  kbass6  32410  dmdmd  32589  atom1d  32642  mdsymlem2  32693  mdsymlem3  32694  mdsymlem4  32695  mdsymlem5  32696  fmptco1f1o  32915  2ndresdju  32931  fnpreimac  32952  fsumiunle  33110  s3f1  33204  swrdf1  33213  dfmgc2lem  33252  dfmgc2  33253  pwrssmgc  33257  mgcf1o  33260  mndlrinvb  33282  mndlactf1  33283  mndractf1  33285  gsummpt2co  33305  gsumwrd2dccatlem  33334  tocyccntz  33401  cycpmconjs  33413  conjga  33427  fxpsubrg  33431  urpropd  33487  elrgspnlem2  33500  elrgspnlem4  33502  elrgspnsubrunlem2  33505  elrgspnsubrun  33506  erler  33522  rlocaddval  33526  rlocmulval  33527  rlocf1  33531  domnprodn0  33535  domnprodeq0  33536  rrgsubm  33541  subrdom  33542  ricdomn1  33546  isdrng4  33555  eqgvscpbl  33609  dvdsruasso  33638  nsgmgclem  33660  nsgmgc  33661  nsgqusf1olem2  33663  nsgqusf1olem3  33664  lmhmqusker  33666  intlidl  33668  rhmquskerlem  33673  elrspunidl  33676  elrspunsn  33677  idlinsubrg  33679  rhmimaidl  33680  drngidl  33681  mxidlprm  33694  mxidlirredi  33695  ssmxidllem  33697  opprlidlabs  33708  qsdrngi  33718  drnglring  33723  dflringlem2  33726  rsprprmprmidl  33753  rsprprmprmidlb  33754  rprmirred  33762  rprmirredb  33763  rprmdvdsprod  33765  1arithidom  33768  1arithufdlem3  33777  1arithufdlem4  33778  deg1prod  33814  r1plmhm  33840  r1pquslmic  33841  0mplrim  33845  selvply1rhmlema  33849  selvply1rhmlem1  33851  selvply1rhm  33856  mplidomlem  33858  extvfvcl  33867  mplvrpmga  33876  mplvrpmmhm  33877  mplvrpmrhm  33878  psrgsum  33879  psrmonprod  33883  esplyfval1  33904  esplyfvaln  33905  vieta  33911  ply1degltdimlem  33953  ply1degltdim  33954  lindsun  33956  lbsdiflsp0  33957  fedgmullem1  33960  fedgmul  33962  lactlmhm  33965  assalactf1o  33966  extdg1id  33997  fldextrspunlsplem  34004  fldextrspunlsp  34005  extdgfialglem2  34024  extdgfialg  34025  minplyirred  34042  algextdeglem8  34055  constrextdg2lem  34079  constrextdg2  34080  constrfiss  34082  constrsdrg  34106  cos9thpiminplylem2  34114  zart0  34210  pstmxmet  34228  ordtconnlem1  34255  esumiun  34425  dya2iocnei  34613  omssubadd  34631  actfunsnf1o  34932  fsum2dsub  34935  reprsuc  34943  reprinfz1  34950  reprpmtf1o  34954  breprexplema  34958  circlemeth  34968  hgt750lemb  34984  cusgr3cyclex  35523  resconn  35633  pibt2  37946  uncf  38133  unccur  38137  fin2so  38141  matunitlindflem1  38150  poimirlem6  38160  poimirlem7  38161  poimirlem25  38179  poimirlem28  38182  poimirlem31  38185  poimirlem32  38186  broucube  38188  ismblfin  38195  mbfposadd  38201  itg2gt0cn  38209  ftc1anclem7  38233  ftc1anc  38235  cover2  38249  indexa  38267  filbcmb  38274  seqpo  38281  incsequz  38282  isbnd2  38317  ghomco  38425  unichnidl  38565  isfldidl  38602  dihvalc  41892  dihvalb  41896  uzindd  42630  aks4d1p8  42739  evlselv  43206  fsuppind  43207  radcnvrat  44909  rexabslelem  46017  rexlimddv2  46422  dvnprodlem2  46546  etransclem46  46879  isgrtri  48590  grlimgrtri  48650  lubeldm2  49612  glbeldm2  49613  thincciso2  50111  aacllem  50457