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  3184  rspc4v  3603  f1elima  7263  fnfvof  7697  frxp3  8149  oecl  8524  oaass  8548  oen0  8574  oeworde  8581  omabs  8639  oiiniseg  9498  cardinfima  10093  fpwwe2lem11  10637  ltmul12a  12082  eluzp1m1  12900  lbzbi  12972  qreccl  13005  xrlttr  13177  elfzodifsumelfzo  13773  quoremnn0  13903  swrdf1  14705  incexc2  15911  mertens  15959  ndvdsadd  16486  nn0seqcvgd  16646  isprm3  16759  isprm7  16785  pcval  16922  prdsval  17526  evlfcl  18296  chnso  18698  ghmqusnsg  19376  ghmquskerlem3  19380  frgpup1  19869  frgpup3lem  19871  ghmcmn  19925  gsumval3  20001  gsumzoppg  20038  ablfaclem2  20182  gsumdixp  20426  isdrng4  20869  suborng  21009  drngidl  21415  rhmpreimaidl  21446  rhmqusnsg  21455  prmidl2  21496  idlmulssprm  21497  isprmidlc  21502  rhmpreimaprmidl  21509  qsidomlem1  21510  qsidomlem2  21511  ssdifidllem  21514  ssdifidlprm  21516  prmidlsubm  21517  frlmgsum  21952  psrass1lem  22113  psrass1  22143  psdmul  22359  evls1maplmhm  22567  m2cpminvid2  22942  pmatcollpw2lem  22964  chcoeffeqlem  23072  neissex  23314  neiptopnei  23319  dissnlocfin  23717  tx1stc  23838  kqreglem1  23929  xpstopnlem1  23997  alexsublem  24232  metuel2  24753  icoopnst  25129  iocopnst  25130  volcn  25796  mbflimsup  25856  mbflim  25858  itg1addlem4  25889  itg1addlem5  25890  itg1climres  25904  limcflf  26071  dvcobr  26136  dvcnvlem  26166  dvfsumge  26212  mdegmullem  26266  plyeq0lem  26398  plypf1  26400  mtestbdd  26599  mbfulm  26600  fsumdvdscom  27380  muinv  27388  logfaclbnd  27417  logexprlim  27420  dchrinv  27456  lgsval3  27510  2sqmo  27632  rpvmasum2  27707  dchrisum0lem1  27711  dchrisum0  27715  selberg  27743  selberg3lem1  27752  selberg34r  27766  pntsval2  27771  nosupbnd1lem5  27907  noinfbnd1lem5  27922  nocvxminlem  27978  oldbday  28125  peano5uzs  28628  iscgrglt  28814  ercgrg  28817  legso  28899  tglinesseq  28944  tglnpt3  28958  tglnpt4  28959  oppperpex  29065  hpgerlem  29078  isplng  29091  plngrotlem3  29102  plng3p  29110  trgcopyeu  29148  dfcgra2  29172  ragcgra  29177  inaghl  29193  prlnghpg  29227  dfprlng2  29228  dfprlng3  29229  prlngex  29232  prlngmolem1  29233  prlngmolem2  29234  quadcgrprlng  29247  colinearalg  29291  axeuclid  29344  axcontlem2  29346  axcontlem7  29351  wlkiswwlksupgr2  30269  grpoidinvlem4  30906  ipblnfi  31254  shmodsi  31788  eighmorth  32363  kbass5  32519  kbass6  32520  dmdmd  32699  atom1d  32752  mdsymlem2  32803  mdsymlem3  32804  mdsymlem4  32805  mdsymlem5  32806  fmptco1f1o  33025  2ndresdju  33041  fnpreimac  33062  fsumiunle  33219  s3f1  33310  dfmgc2lem  33355  dfmgc2  33356  pwrssmgc  33360  mgcf1o  33363  mndlrinvb  33385  mndlactf1  33386  mndractf1  33388  gsummpt2co  33408  gsumwrd2dccatlem  33437  tocyccntz  33504  cycpmconjs  33516  conjga  33530  fxpsubrg  33534  urpropd  33590  elrgspnlem2  33603  elrgspnlem4  33605  elrgspnsubrunlem2  33608  elrgspnsubrun  33609  erler  33625  rlocaddval  33629  rlocmulval  33630  rlocf1  33634  domnprodn0  33638  domnprodeq0  33639  rrgsubm  33644  subrdom  33645  ricdomn1  33649  eqgvscpbl  33710  dvdsruasso  33738  nsgmgclem  33760  nsgmgc  33761  nsgqusf1olem2  33763  nsgqusf1olem3  33764  lmhmqusker  33766  intlidl  33768  rhmquskerlem  33773  elrspunidl  33776  elrspunsn  33777  idlinsubrg  33779  rhmimaidl  33780  mxidlprm  33793  mxidlirredi  33794  ssmxidllem  33796  opprlidlabs  33807  qsdrngi  33817  drnglring  33822  dflringlem2  33825  rsprprmprmidl  33852  rsprprmprmidlb  33853  rprmirred  33861  rprmirredb  33862  rprmdvdsprod  33864  1arithidom  33867  1arithufdlem3  33876  1arithufdlem4  33877  deg1prod  33913  r1plmhm  33939  r1pquslmic  33940  0mplrim  33944  selvply1rhmlema  33948  selvply1rhmlem1  33950  selvply1rhm  33955  mplidomlem  33957  extvfvcl  33966  mplvrpmga  33975  mplvrpmmhm  33976  mplvrpmrhm  33977  psrgsum  33978  psrmonprod  33982  esplyfval1  34003  esplyfvaln  34004  vieta  34010  ply1degltdimlem  34052  ply1degltdim  34053  lindsun  34055  lbsdiflsp0  34056  fedgmullem1  34059  fedgmul  34061  lactlmhm  34064  assalactf1o  34065  extdg1id  34096  fldextrspunlsplem  34103  fldextrspunlsp  34104  extdgfialglem2  34123  extdgfialg  34124  minplyirred  34141  algextdeglem8  34154  constrextdg2lem  34178  constrextdg2  34179  constrfiss  34181  constrsdrg  34205  cos9thpiminplylem2  34213  zart0  34309  pstmxmet  34327  ordtconnlem1  34354  esumiun  34524  dya2iocnei  34713  omssubadd  34731  actfunsnf1o  35032  fsum2dsub  35035  reprsuc  35043  reprinfz1  35050  reprpmtf1o  35054  breprexplema  35058  circlemeth  35068  hgt750lemb  35084  cusgr3cyclex  35645  resconn  35751  pibt2  38096  uncf  38283  unccur  38287  fin2so  38291  matunitlindflem1  38300  poimirlem6  38310  poimirlem7  38311  poimirlem25  38329  poimirlem28  38332  poimirlem31  38335  poimirlem32  38336  broucube  38338  ismblfin  38345  mbfposadd  38351  itg2gt0cn  38359  ftc1anclem7  38383  ftc1anc  38385  cover2  38399  indexa  38417  filbcmb  38424  seqpo  38431  incsequz  38432  isbnd2  38467  ghomco  38575  unichnidl  38715  isfldidl  38752  dihvalc  42040  dihvalb  42044  uzindd  42778  aks4d1p8  42887  evlselv  43354  fsuppind  43355  radcnvrat  45057  rexabslelem  46165  rexlimddv2  46570  dvnprodlem2  46694  etransclem46  47027  isgrtri  48741  grlimgrtri  48801  lubeldm2  49767  glbeldm2  49768  thincciso2  50266  aacllem  50654