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  1380  reximddv3  3182  rspc4v  3602  f1elima  7263  fnfvof  7693  frxp3  8148  oecl  8523  oaass  8547  oen0  8573  oeworde  8580  omabs  8638  oiiniseg  9496  cardinfima  10082  fpwwe2lem11  10627  ltmul12a  12072  eluzp1m1  12889  lbzbi  12961  qreccl  12994  xrlttr  13166  elfzodifsumelfzo  13762  quoremnn0  13891  incexc2  15894  mertens  15942  ndvdsadd  16469  nn0seqcvgd  16629  isprm3  16742  isprm7  16768  pcval  16905  prdsval  17509  evlfcl  18279  chnso  18681  ghmqusnsg  19353  ghmquskerlem3  19357  frgpup1  19846  frgpup3lem  19848  ghmcmn  19902  gsumval3  19978  gsumzoppg  20015  ablfaclem2  20159  gsumdixp  20401  isdrng4  20826  suborng  20960  drngidl  21366  rhmpreimaidl  21397  rhmqusnsg  21406  prmidl2  21447  idlmulssprm  21448  isprmidlc  21453  rhmpreimaprmidl  21460  qsidomlem1  21461  qsidomlem2  21462  ssdifidllem  21465  ssdifidlprm  21467  prmidlsubm  21468  frlmgsum  21903  psrass1lem  22064  psrass1  22094  psdmul  22310  evls1maplmhm  22518  m2cpminvid2  22893  pmatcollpw2lem  22915  chcoeffeqlem  23023  neissex  23265  neiptopnei  23270  dissnlocfin  23667  tx1stc  23788  kqreglem1  23879  xpstopnlem1  23947  alexsublem  24182  metuel2  24703  icoopnst  25079  iocopnst  25080  volcn  25746  mbflimsup  25806  mbflim  25808  itg1addlem4  25839  itg1addlem5  25840  itg1climres  25854  limcflf  26021  dvcobr  26086  dvcnvlem  26116  dvfsumge  26162  mdegmullem  26216  plyeq0lem  26348  plypf1  26350  mtestbdd  26549  mbfulm  26550  fsumdvdscom  27330  muinv  27338  logfaclbnd  27367  logexprlim  27370  dchrinv  27406  lgsval3  27460  2sqmo  27582  rpvmasum2  27657  dchrisum0lem1  27661  dchrisum0  27665  selberg  27693  selberg3lem1  27702  selberg34r  27716  pntsval2  27721  nosupbnd1lem5  27857  noinfbnd1lem5  27872  nocvxminlem  27928  oldbday  28075  peano5uzs  28578  iscgrglt  28764  ercgrg  28767  legso  28849  tglinesseq  28894  tglnpt3  28908  tglnpt4  28909  oppperpex  29015  hpgerlem  29028  isplng  29041  plngrotlem3  29052  plng3p  29060  trgcopyeu  29098  dfcgra2  29122  ragcgra  29127  inaghl  29143  prlnghpg  29177  dfprlng2  29178  dfprlng3  29179  prlngex  29182  prlngmolem1  29183  prlngmolem2  29184  quadcgrprlng  29197  colinearalg  29241  axeuclid  29294  axcontlem2  29296  axcontlem7  29301  wlkiswwlksupgr2  30207  grpoidinvlem4  30840  ipblnfi  31188  shmodsi  31722  eighmorth  32297  kbass5  32453  kbass6  32454  dmdmd  32633  atom1d  32686  mdsymlem2  32737  mdsymlem3  32738  mdsymlem4  32739  mdsymlem5  32740  fmptco1f1o  32959  2ndresdju  32975  fnpreimac  32996  fsumiunle  33154  s3f1  33248  swrdf1  33257  dfmgc2lem  33296  dfmgc2  33297  pwrssmgc  33301  mgcf1o  33304  mndlrinvb  33326  mndlactf1  33327  mndractf1  33329  gsummpt2co  33349  gsumwrd2dccatlem  33378  tocyccntz  33445  cycpmconjs  33457  conjga  33471  fxpsubrg  33475  urpropd  33531  elrgspnlem2  33544  elrgspnlem4  33546  elrgspnsubrunlem2  33549  elrgspnsubrun  33550  erler  33566  rlocaddval  33570  rlocmulval  33571  rlocf1  33575  domnprodn0  33579  domnprodeq0  33580  rrgsubm  33585  subrdom  33586  ricdomn1  33590  eqgvscpbl  33651  dvdsruasso  33679  nsgmgclem  33701  nsgmgc  33702  nsgqusf1olem2  33704  nsgqusf1olem3  33705  lmhmqusker  33707  intlidl  33709  rhmquskerlem  33714  elrspunidl  33717  elrspunsn  33718  idlinsubrg  33720  rhmimaidl  33721  mxidlprm  33734  mxidlirredi  33735  ssmxidllem  33737  opprlidlabs  33748  qsdrngi  33758  drnglring  33763  dflringlem2  33766  rsprprmprmidl  33793  rsprprmprmidlb  33794  rprmirred  33802  rprmirredb  33803  rprmdvdsprod  33805  1arithidom  33808  1arithufdlem3  33817  1arithufdlem4  33818  deg1prod  33854  r1plmhm  33880  r1pquslmic  33881  0mplrim  33885  selvply1rhmlema  33889  selvply1rhmlem1  33891  selvply1rhm  33896  mplidomlem  33898  extvfvcl  33907  mplvrpmga  33916  mplvrpmmhm  33917  mplvrpmrhm  33918  psrgsum  33919  psrmonprod  33923  esplyfval1  33944  esplyfvaln  33945  vieta  33951  ply1degltdimlem  33993  ply1degltdim  33994  lindsun  33996  lbsdiflsp0  33997  fedgmullem1  34000  fedgmul  34002  lactlmhm  34005  assalactf1o  34006  extdg1id  34037  fldextrspunlsplem  34044  fldextrspunlsp  34045  extdgfialglem2  34064  extdgfialg  34065  minplyirred  34082  algextdeglem8  34095  constrextdg2lem  34119  constrextdg2  34120  constrfiss  34122  constrsdrg  34146  cos9thpiminplylem2  34154  zart0  34250  pstmxmet  34268  ordtconnlem1  34295  esumiun  34465  dya2iocnei  34653  omssubadd  34671  actfunsnf1o  34972  fsum2dsub  34975  reprsuc  34983  reprinfz1  34990  reprpmtf1o  34994  breprexplema  34998  circlemeth  35008  hgt750lemb  35024  cusgr3cyclex  35609  resconn  35719  pibt2  38044  uncf  38231  unccur  38235  fin2so  38239  matunitlindflem1  38248  poimirlem6  38258  poimirlem7  38259  poimirlem25  38277  poimirlem28  38280  poimirlem31  38283  poimirlem32  38284  broucube  38286  ismblfin  38293  mbfposadd  38299  itg2gt0cn  38307  ftc1anclem7  38331  ftc1anc  38333  cover2  38347  indexa  38365  filbcmb  38372  seqpo  38379  incsequz  38380  isbnd2  38415  ghomco  38523  unichnidl  38663  isfldidl  38700  dihvalc  41988  dihvalb  41992  uzindd  42726  aks4d1p8  42835  evlselv  43304  fsuppind  43305  radcnvrat  45007  rexabslelem  46115  rexlimddv2  46520  dvnprodlem2  46644  etransclem46  46977  isgrtri  48691  grlimgrtri  48751  lubeldm2  49717  glbeldm2  49718  thincciso2  50216  aacllem  50584