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  3179  rspc4v  3596  f1elima  7260  fnfvof  7695  frxp3  8149  oecl  8524  oaass  8548  oen0  8574  oeworde  8581  omabs  8639  uncf  8870  oiiniseg  9505  cardinfima  10100  fpwwe2lem11  10650  ltmul12a  12095  eluzp1m1  12913  lbzbi  12985  qreccl  13019  xrlttr  13191  elfzodifsumelfzo  13787  quoremnn0  13917  swrdf1  14719  incexc2  15927  mertens  15975  ndvdsadd  16500  nn0seqcvgd  16660  isprm3  16773  isprm7  16799  pcval  16936  prdsval  17540  evlfcl  18310  chnso  18712  ghmqusnsg  19409  ghmquskerlem3  19413  frgpup1  19902  frgpup3lem  19904  ghmcmn  19958  gsumval3  20034  gsumzoppg  20071  ablfaclem2  20215  gsumdixp  20459  isdrng4  20902  suborng  21042  drngidl  21448  rhmpreimaidl  21479  rhmqusnsg  21488  prmidl2  21529  idlmulssprm  21530  isprmidlc  21535  rhmpreimaprmidl  21542  qsidomlem1  21543  qsidomlem2  21544  ssdifidllem  21547  ssdifidlprm  21549  prmidlsubm  21550  frlmgsum  21985  psrass1lem  22148  psrass1  22178  psdmul  22394  evls1maplmhm  22602  matunitlindflem1  22901  m2cpminvid2  22980  pmatcollpw2lem  23002  chcoeffeqlem  23110  neissex  23352  neiptopnei  23357  dissnlocfin  23755  tx1stc  23876  kqreglem1  23967  xpstopnlem1  24035  alexsublem  24270  metuel2  24791  icoopnst  25167  iocopnst  25168  volcn  25834  mbflimsup  25894  mbflim  25896  itg1addlem4  25927  itg1addlem5  25928  itg1climres  25942  limcflf  26108  dvcobr  26173  dvcnvlem  26203  dvfsumge  26249  mdegmullem  26303  plyeq0lem  26436  plypf1  26438  mtestbdd  26641  mbfulm  26642  fsumdvdscom  27421  muinv  27429  logfaclbnd  27458  logexprlim  27461  dchrinv  27497  lgsval3  27551  2sqmo  27673  rpvmasum2  27748  dchrisum0lem1  27752  dchrisum0  27756  selberg  27784  selberg3lem1  27793  selberg34r  27807  pntsval2  27812  nosupbnd1lem5  27948  noinfbnd1lem5  27963  nocvxminlem  28019  oldbday  28166  peano5uzs  28669  tgsegconeu  28828  iscgrglt  28856  ercgrg  28859  legso  28941  tglinesseq  28987  tglnpt3  29001  tglnpt4  29002  oppperpex  29108  hpgerlem  29122  isplng  29135  plngrotlem3  29146  plng3p  29154  trgcopyeu  29192  zerocgra  29210  dfcgra2  29217  ragcgra  29222  tgaaddcpbllem1  29228  tgaaddcpbl  29231  inaghl  29243  cgraer  29256  angmgmaddeu1  29258  angmgmaddeu2  29259  angmgmaddeu3  29260  angmgmaddeu4  29261  angmgmaddeu5  29262  angmgmaddeu6  29263  angmgmaddeu7  29264  angmgmaddov2lem  29266  angmgmaddov1  29267  angmgmaddov2  29268  angmgmaddcpbl  29269  angmgmaddcl  29270  angmgmaddlid  29271  angmgmaddrid  29272  prlnghpg  29303  dfprlng2  29304  dfprlng3  29305  prlngex  29308  prlngmolem1  29309  prlngmolem2  29310  quadcgrprlng  29323  colinearalg  29367  axeuclid  29420  axcontlem2  29422  axcontlem7  29427  wlkiswwlksupgr2  30345  grpoidinvlem4  30988  ipblnfi  31336  shmodsi  31870  eighmorth  32445  kbass5  32601  kbass6  32602  dmdmd  32781  atom1d  32834  mdsymlem2  32885  mdsymlem3  32886  mdsymlem4  32887  mdsymlem5  32888  fmptco1f1o  33106  2ndresdju  33122  fnpreimac  33143  fsumiunle  33299  s3f1  33390  dfmgc2lem  33435  dfmgc2  33436  pwrssmgc  33440  mgcf1o  33443  mndlrinvb  33465  mndlactf1  33466  mndractf1  33468  gsummpt2co  33488  gsumwrd2dccatlem  33517  tocyccntz  33584  cycpmconjs  33596  conjga  33610  fxpsubrg  33614  urpropd  33670  elrgspnlem2  33683  elrgspnlem4  33685  elrgspnsubrunlem2  33688  elrgspnsubrun  33689  erler  33705  rlocaddval  33709  rlocmulval  33710  rlocf1  33714  domnprodn0  33718  domnprodeq0  33719  rrgsubm  33724  subrdom  33725  ricdomn1  33729  eqgvscpbl  33790  dvdsruasso  33818  nsgmgclem  33840  nsgmgc  33841  nsgqusf1olem2  33843  nsgqusf1olem3  33844  lmhmqusker  33846  intlidl  33848  rhmquskerlem  33853  elrspunidl  33856  elrspunsn  33857  idlinsubrg  33859  rhmimaidl  33860  mxidlprm  33873  mxidlirredi  33874  ssmxidllem  33876  opprlidlabs  33887  qsdrngi  33897  drnglring  33902  dflringlem2  33905  rsprprmprmidl  33932  rsprprmprmidlb  33933  rprmirred  33941  rprmirredb  33942  rprmdvdsprod  33944  1arithidom  33947  1arithufdlem3  33956  1arithufdlem4  33957  deg1prod  33993  r1plmhm  34019  r1pquslmic  34020  0mplrim  34024  selvply1rhmlema  34028  selvply1rhmlem1  34030  selvply1rhm  34035  mplidomlem  34037  extvfvcl  34046  mplvrpmga  34055  mplvrpmmhm  34056  mplvrpmrhm  34057  psrgsum  34058  psrmonprod  34062  esplyfval1  34083  esplyfvaln  34084  vieta  34090  ply1degltdimlem  34132  ply1degltdim  34133  lindsun  34135  lbsdiflsp0  34136  fedgmullem1  34139  fedgmul  34141  lactlmhm  34144  assalactf1o  34145  extdg1id  34176  fldextrspunlsplem  34183  fldextrspunlsp  34184  extdgfialglem2  34203  extdgfialg  34204  minplyirred  34221  algextdeglem8  34234  constrextdg2lem  34258  constrextdg2  34259  constrfiss  34261  constrsdrg  34285  cos9thpiminplylem2  34293  zart0  34389  pstmxmet  34407  ordtconnlem1  34434  esumiun  34604  dya2iocnei  34793  omssubadd  34811  actfunsnf1o  35112  fsum2dsub  35115  reprsuc  35123  reprinfz1  35130  reprpmtf1o  35134  breprexplema  35138  circlemeth  35148  hgt750lemb  35164  cusgr3cyclex  35725  resconn  35825  pibt2  38171  unccur  38357  fin2so  38361  poimirlem6  38375  poimirlem7  38376  poimirlem25  38394  poimirlem28  38397  poimirlem31  38400  poimirlem32  38401  broucube  38403  ismblfin  38410  mbfposadd  38416  itg2gt0cn  38424  ftc1anclem7  38448  ftc1anc  38450  cover2  38465  indexa  38483  filbcmb  38490  seqpo  38497  incsequz  38498  isbnd2  38533  ghomco  38641  unichnidl  38781  isfldidl  38818  dihvalc  42106  dihvalb  42110  uzindd  42844  aks4d1p8  42953  evlselv  43435  fsuppind  43436  radcnvrat  45138  rexabslelem  46246  rexlimddv2  46651  dvnprodlem2  46775  etransclem46  47108  isgrtri  48859  grlimgrtri  48919  lubeldm2  49882  glbeldm2  49883  thincciso2  50381  aacllem  50772