MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anasss Structured version   Visualization version   GIF version

Theorem anasss 680
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
StepHypRef Expression
1 anasss.1 . . 3 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
21exp31 629 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 448 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  anass  682  anabss3  881  f1elima  6560  fnfvof  6953  oecl  7662  oaass  7686  oen0  7711  oeworde  7718  omabs  7772  oiiniseg  8479  cardinfima  8958  fpwwe2lem12  9501  ltmul12a  10917  eluzp1m1  11749  lbzbi  11814  qreccl  11846  xrlttr  12011  elfzodifsumelfzo  12573  quoremnn0  12695  incexc2  14614  mertens  14662  ndvdsadd  15181  nn0seqcvgd  15330  isprm3  15443  isprm7  15467  pcval  15596  prdsval  16162  evlfcl  16909  frgpup1  18234  frgpup3lem  18236  ghmcmn  18283  gsumval3  18354  gsumzoppg  18390  ablfaclem2  18531  gsumdixp  18655  psrass1lem  19425  psrass1  19453  frlmgsum  20159  m2cpminvid2  20608  pmatcollpw2lem  20630  chcoeffeqlem  20738  neissex  20979  neiptopnei  20984  dissnlocfin  21380  tx1stc  21501  kqreglem1  21592  xpstopnlem1  21660  alexsublem  21895  metuel2  22417  icoopnst  22785  iocopnst  22786  volcn  23420  mbflimsup  23478  mbflim  23480  itg1addlem4  23511  itg1addlem5  23512  itg1climres  23526  limcflf  23690  dvcobr  23754  dvcnvlem  23784  dvfsumge  23830  mdegmullem  23883  plyeq0lem  24011  plypf1  24013  mtestbdd  24204  mbfulm  24205  fsumdvdscom  24956  muinv  24964  logfaclbnd  24992  logexprlim  24995  dchrinv  25031  lgsval3  25085  rpvmasum2  25246  dchrisum0lem1  25250  dchrisum0  25254  selberg  25282  selberg3lem1  25291  selberg34r  25305  pntsval2  25310  iscgrglt  25454  ercgrg  25457  legso  25539  oppperpex  25690  outpasch  25692  hpgerlem  25702  trgcopyeu  25743  dfcgra2  25766  inaghl  25776  colinearalg  25835  axeuclid  25888  axcontlem2  25890  axcontlem7  25895  wlkiswwlksupgr2  26831  grpoidinvlem4  27489  ipblnfi  27839  shmodsi  28376  eighmorth  28951  kbass5  29107  kbass6  29108  dmdmd  29287  atom1d  29340  mdsymlem2  29391  mdsymlem3  29392  mdsymlem4  29393  mdsymlem5  29394  fmptco1f1o  29562  fsumiunle  29703  2sqmo  29777  gsummpt2co  29908  suborng  29943  pstmxmet  30068  ordtconnlem1  30098  esumiun  30284  dya2iocnei  30472  omssubadd  30490  actfunsnf1o  30810  fsum2dsub  30813  reprsuc  30821  reprinfz1  30828  reprpmtf1o  30832  breprexplema  30836  circlemeth  30846  hgt750lemb  30862  resconn  31354  nosupbnd1lem5  31983  nocvxminlem  32018  uncf  33518  unccur  33522  fin2so  33526  matunitlindflem1  33535  poimirlem6  33545  poimirlem7  33546  poimirlem25  33564  poimirlem28  33567  poimirlem31  33570  poimirlem32  33571  broucube  33573  ismblfin  33580  mbfposadd  33587  itg2gt0cn  33595  ftc1anclem7  33621  ftc1anc  33623  cover2  33638  indexa  33658  filbcmb  33665  seqpo  33673  incsequz  33674  isbnd2  33712  ghomco  33820  unichnidl  33960  isfldidl  33997  dihvalc  36839  dihvalb  36843  radcnvrat  38830  reximddv3  39657  rexabslelem  39958  rexlimddv2  40367  dvnprodlem2  40480  etransclem46  40815  aacllem  42875
  Copyright terms: Public domain W3C validator