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

Theorem anasss 676
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 627 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 447 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  anass  678  anabss3  859  f1elima  6395  fnfvof  6782  oecl  7477  oaass  7501  oen0  7526  oeworde  7533  omabs  7587  oiiniseg  8294  cardinfima  8776  fpwwe2lem12  9315  ltmul12a  10724  eluzp1m1  11539  lbzbi  11604  qreccl  11636  xrlttr  11804  elfzodifsumelfzo  12352  quoremnn0  12468  incexc2  14351  mertens  14399  ndvdsadd  14914  nn0seqcvgd  15063  isprm3  15176  isprm7  15200  pcval  15329  prdsval  15880  evlfcl  16627  frgpup1  17953  frgpup3lem  17955  ghmcmn  18002  gsumval3  18073  gsumzoppg  18109  ablfaclem2  18250  gsumdixp  18374  psrass1lem  19140  psrass1  19168  frlmgsum  19868  m2cpminvid2  20317  pmatcollpw2lem  20339  chcoeffeqlem  20447  neissex  20679  neiptopnei  20684  dissnlocfin  21080  tx1stc  21201  kqreglem1  21292  xpstopnlem1  21360  alexsublem  21596  metuel2  22117  icoopnst  22473  iocopnst  22474  volcn  23093  mbflimsup  23152  mbflim  23154  itg1addlem4  23185  itg1addlem5  23186  itg1climres  23200  limcflf  23364  dvcobr  23428  dvcnvlem  23456  dvfsumge  23502  mdegmullem  23555  plyeq0lem  23683  plypf1  23685  mtestbdd  23876  mbfulm  23877  fsumdvdscom  24624  muinv  24632  logfaclbnd  24660  logexprlim  24663  dchrinv  24699  lgsval3  24753  rpvmasum2  24914  dchrisum0lem1  24918  dchrisum0  24922  selberg  24950  selberg3lem1  24959  selberg34r  24973  pntsval2  24978  iscgrglt  25123  ercgrg  25126  legso  25208  oppperpex  25359  outpasch  25361  hpgerlem  25371  trgcopyeu  25412  dfcgra2  25435  inaghl  25445  colinearalg  25504  axeuclid  25557  axcontlem2  25559  axcontlem7  25564  grpoidinvlem4  26507  ipblnfi  26897  shmodsi  27434  eighmorth  28009  kbass5  28165  kbass6  28166  dmdmd  28345  atom1d  28398  mdsymlem2  28449  mdsymlem3  28450  mdsymlem4  28451  mdsymlem5  28452  2sqmo  28782  gsummpt2co  28913  suborng  28948  pstmxmet  29070  ordtconlem1  29100  esumiun  29285  dya2iocnei  29473  omssubadd  29491  rescon  30284  nocvxminlem  30891  nobndlem6  30898  uncf  32357  unccur  32361  fin2so  32365  matunitlindflem1  32374  poimirlem6  32384  poimirlem7  32385  poimirlem25  32403  poimirlem28  32406  poimirlem31  32409  poimirlem32  32410  broucube  32412  ismblfin  32419  mbfposadd  32426  itg2gt0cn  32434  ftc1anclem7  32460  ftc1anc  32462  cover2  32477  indexa  32497  filbcmb  32504  seqpo  32512  incsequz  32513  isbnd2  32551  ghomco  32659  unichnidl  32799  isfldidl  32836  dihvalc  35339  dihvalb  35343  radcnvrat  37334  dvnprodlem2  38637  etransclem46  38973  1wlkiswwlksupgr2  41072  aacllem  42315
  Copyright terms: Public domain W3C validator