Theorem anasss 472

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anass  474  anabss3  688  biadanid  835  3anasss  1380  reximddv3  3180  rspc4v  3596  f1elima  7265  fnfvof  7708  frxp3  8161  oecl  8538  oaass  8562  oen0  8588  oeworde  8595  omabs  8653  uncf  8884  oiiniseg  9520  cardinfima  10169  fpwwe2lem11  10719  ltmul12a  12166  eluzp1m1  12984  lbzbi  13056  qreccl  13090  xrlttr  13262  elfzodifsumelfzo  13859  quoremnn0  13989  swrdf1  14792  incexc2  16000  mertens  16048  ndvdsadd  16573  nn0seqcvgd  16738  isprm3  16851  isprm7  16877  pcval  17015  prdsval  17619  evlfcl  18389  chnso  18791  ghmqusnsg  19489  ghmquskerlem3  19493  frgpup1  19982  frgpup3lem  19984  ghmcmn  20038  gsumval3  20114  gsumzoppg  20151  ablfaclem2  20295  gsumdixp  20541  isdrng4  20985  suborng  21126  drngidl  21532  rhmpreimaidl  21564  rhmqusnsg  21574  prmidl2  21615  idlmulssprm  21616  isprmidlc  21621  rhmpreimaprmidl  21628  qsidomlem1  21629  qsidomlem2  21630  ssdifidllem  21633  ssdifidlprm  21635  prmidlsubm  21636  frlmgsum  22071  psrass1lem  22234  psrass1  22264  psdmul  22480  evls1maplmhm  22688  matunitlindflem1  22987  m2cpminvid2  23066  pmatcollpw2lem  23088  chcoeffeqlem  23196  neissex  23438  neiptopnei  23443  dissnlocfin  23841  tx1stc  23962  kqreglem1  24053  xpstopnlem1  24121  alexsublem  24356  metuel2  24877  icoopnst  25253  iocopnst  25254  volcn  25920  mbflimsup  25980  mbflim  25982  itg1addlem4  26013  itg1addlem5  26014  itg1climres  26028  limcflf  26194  dvcobr  26259  dvcnvlem  26289  dvfsumge  26335  mdegmullem  26389  plyeq0lem  26522  plypf1  26524  mtestbdd  26725  mbfulm  26726  fsumdvdscom  27505  muinv  27513  logfaclbnd  27542  logexprlim  27545  dchrinv  27581  lgsval3  27635  2sqmo  27757  rpvmasum2  27832  dchrisum0lem1  27836  dchrisum0  27840  selberg  27868  selberg3lem1  27877  selberg34r  27891  pntsval2  27896  nosupbnd1lem5  28062  noinfbnd1lem5  28077  nocvxminlem  28133  oldbday  28280  peano5uzs  28783  tgsegconeu  28942  iscgrglt  28970  ercgrg  28973  legso  29055  tglinesseq  29101  tglnpt3  29115  tglnpt4  29116  oppperpex  29222  hpgerlem  29236  isplng  29249  plngrotlem3  29260  plng3p  29268  trgcopyeu  29306  zerocgra  29324  dfcgra2  29331  ragcgra  29336  tgaaddcpbllem1  29342  tgaaddcpbl  29345  inaghl  29357  cgraer  29370  angmgmaddeu1  29372  angmgmaddeu2  29373  angmgmaddeu3  29374  angmgmaddeu4  29375  angmgmaddeu5  29376  angmgmaddeu6  29377  angmgmaddeu7  29378  angmgmaddov2lem  29380  angmgmaddov1  29381  angmgmaddov2  29382  angmgmaddcpbl  29383  angmgmaddcl  29384  angmgmaddlid  29385  angmgmaddrid  29386  prlnghpg  29417  dfprlng2  29418  dfprlng3  29419  prlngex  29422  prlngmolem1  29423  prlngmolem2  29424  quadcgrprlng  29437  colinearalg  29481  axeuclid  29534  axcontlem2  29536  axcontlem7  29541  wlkiswwlksupgr2  30459  grpoidinvlem4  31102  ipblnfi  31450  shmodsi  31984  eighmorth  32559  kbass5  32715  kbass6  32716  dmdmd  32895  atom1d  32948  mdsymlem2  32999  mdsymlem3  33000  mdsymlem4  33001  mdsymlem5  33002  fmptco1f1o  33220  2ndresdju  33236  fnpreimac  33257  fsumiunle  33413  s3f1  33504  dfmgc2lem  33549  dfmgc2  33550  pwrssmgc  33554  mgcf1o  33557  mndlrinvb  33579  mndlactf1  33580  mndractf1  33582  gsummpt2co  33602  gsumwrd2dccatlem  33631  tocyccntz  33698  cycpmconjs  33710  conjga  33724  fxpsubrg  33728  urpropd  33784  elrgspnlem2  33797  elrgspnlem4  33799  elrgspnsubrunlem2  33802  elrgspnsubrun  33803  erler  33819  rlocaddval  33823  rlocmulval  33824  rlocf1  33828  domnprodn0  33832  domnprodeq0  33833  rrgsubm  33838  subrdom  33839  ricdomn1  33843  eqgvscpbl  33904  dvdsruasso  33933  nsgmgclem  33955  nsgmgc  33956  nsgqusf1olem2  33958  nsgqusf1olem3  33959  lmhmqusker  33961  intlidl  33963  rhmquskerlem  33968  elrspunidl  33971  elrspunsn  33972  idlinsubrg  33974  rhmimaidl  33975  mxidlprm  33988  mxidlirredi  33989  ssmxidllem  33991  opprlidlabs  34002  qsdrngi  34012  drnglring  34017  dflringlem2  34020  rsprprmprmidl  34047  rsprprmprmidlb  34048  rprmirred  34056  rprmirredb  34057  rprmdvdsprod  34059  1arithidom  34062  1arithufdlem3  34071  1arithufdlem4  34072  deg1prod  34108  r1plmhm  34134  r1pquslmic  34135  0mplrim  34139  selvply1rhmlema  34143  selvply1rhmlem1  34145  selvply1rhm  34150  mplidomlem  34152  extvfvcl  34161  mplvrpmga  34170  mplvrpmmhm  34171  mplvrpmrhm  34172  psrgsum  34173  psrmonprod  34177  esplyfval1  34198  esplyfvaln  34199  vieta  34205  ply1degltdimlem  34247  ply1degltdim  34248  lindsun  34250  lbsdiflsp0  34251  fedgmullem1  34254  fedgmul  34256  lactlmhm  34259  assalactf1o  34260  extdg1id  34291  fldextrspunlsplem  34298  fldextrspunlsp  34299  extdgfialglem2  34318  extdgfialg  34319  minplyirred  34336  algextdeglem8  34349  constrextdg2lem  34373  constrextdg2  34374  constrfiss  34376  constrsdrg  34400  cos9thpiminplylem2  34408  zart0  34504  pstmxmet  34522  ordtconnlem1  34549  esumiun  34719  dya2iocnei  34907  omssubadd  34925  actfunsnf1o  35226  fsum2dsub  35229  reprsuc  35237  reprinfz1  35244  reprpmtf1o  35248  breprexplema  35252  circlemeth  35262  hgt750lemb  35278  cusgr3cyclex  35890  resconn  35990  pibt2  38320  unccur  38506  fin2so  38510  poimirlem6  38524  poimirlem7  38525  poimirlem25  38543  poimirlem28  38546  poimirlem31  38549  poimirlem32  38550  broucube  38552  ismblfin  38559  mbfposadd  38565  itg2gt0cn  38573  ftc1anclem7  38597  ftc1anc  38599  cover2  38629  indexa  38647  filbcmb  38654  seqpo  38661  incsequz  38662  isbnd2  38697  ghomco  38805  unichnidl  38945  isfldidl  38982  dihvalc  42270  dihvalb  42274  uzindd  43008  aks4d1p8  43117  evlselv  43597  fsuppind  43598  radcnvrat  45283  rexabslelem  46397  rexlimddv2  46802  dvnprodlem2  46926  etransclem46  47259  isgrtri  49010  grlimgrtri  49070  lubeldm2  50033  glbeldm2  50034  thincciso2  50532  aacllem  50908