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

Theorem anasss 678
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 449 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  anass  680  anabss3  863  f1elima  6505  fnfvof  6896  oecl  7602  oaass  7626  oen0  7651  oeworde  7658  omabs  7712  oiiniseg  8423  cardinfima  8905  fpwwe2lem12  9448  ltmul12a  10864  eluzp1m1  11696  lbzbi  11761  qreccl  11793  xrlttr  11958  elfzodifsumelfzo  12517  quoremnn0  12638  incexc2  14551  mertens  14599  ndvdsadd  15115  nn0seqcvgd  15264  isprm3  15377  isprm7  15401  pcval  15530  prdsval  16096  evlfcl  16843  frgpup1  18169  frgpup3lem  18171  ghmcmn  18218  gsumval3  18289  gsumzoppg  18325  ablfaclem2  18466  gsumdixp  18590  psrass1lem  19358  psrass1  19386  frlmgsum  20092  m2cpminvid2  20541  pmatcollpw2lem  20563  chcoeffeqlem  20671  neissex  20912  neiptopnei  20917  dissnlocfin  21313  tx1stc  21434  kqreglem1  21525  xpstopnlem1  21593  alexsublem  21829  metuel2  22351  icoopnst  22719  iocopnst  22720  volcn  23355  mbflimsup  23414  mbflim  23416  itg1addlem4  23447  itg1addlem5  23448  itg1climres  23462  limcflf  23626  dvcobr  23690  dvcnvlem  23720  dvfsumge  23766  mdegmullem  23819  plyeq0lem  23947  plypf1  23949  mtestbdd  24140  mbfulm  24141  fsumdvdscom  24892  muinv  24900  logfaclbnd  24928  logexprlim  24931  dchrinv  24967  lgsval3  25021  rpvmasum2  25182  dchrisum0lem1  25186  dchrisum0  25190  selberg  25218  selberg3lem1  25227  selberg34r  25241  pntsval2  25246  iscgrglt  25390  ercgrg  25393  legso  25475  oppperpex  25626  outpasch  25628  hpgerlem  25638  trgcopyeu  25679  dfcgra2  25702  inaghl  25712  colinearalg  25771  axeuclid  25824  axcontlem2  25826  axcontlem7  25831  wlkiswwlksupgr2  26744  grpoidinvlem4  27331  ipblnfi  27681  shmodsi  28218  eighmorth  28793  kbass5  28949  kbass6  28950  dmdmd  29129  atom1d  29182  mdsymlem2  29233  mdsymlem3  29234  mdsymlem4  29235  mdsymlem5  29236  fmptco1f1o  29407  fsumiunle  29549  2sqmo  29623  gsummpt2co  29754  suborng  29789  pstmxmet  29914  ordtconnlem1  29944  esumiun  30130  dya2iocnei  30318  omssubadd  30336  actfunsnf1o  30656  fsum2dsub  30659  reprsuc  30667  reprinfz1  30674  reprpmtf1o  30678  breprexplema  30682  circlemeth  30692  hgt750lemb  30708  resconn  31202  nosupbnd1lem5  31832  nocvxminlem  31867  uncf  33359  unccur  33363  fin2so  33367  matunitlindflem1  33376  poimirlem6  33386  poimirlem7  33387  poimirlem25  33405  poimirlem28  33408  poimirlem31  33411  poimirlem32  33412  broucube  33414  ismblfin  33421  mbfposadd  33428  itg2gt0cn  33436  ftc1anclem7  33462  ftc1anc  33464  cover2  33479  indexa  33499  filbcmb  33506  seqpo  33514  incsequz  33515  isbnd2  33553  ghomco  33661  unichnidl  33801  isfldidl  33838  dihvalc  36341  dihvalb  36345  radcnvrat  38333  rexabslelem  39458  dvnprodlem2  39925  etransclem46  40260  aacllem  42312
  Copyright terms: Public domain W3C validator