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

Theorem anasss 454
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 408 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 407 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 198  df-an 385
This theorem is referenced by:  anass  456  anabss3  657  f1elima  6740  fnfvof  7137  oecl  7850  oaass  7874  oen0  7899  oeworde  7906  omabs  7960  oiiniseg  8673  cardinfima  9199  fpwwe2lem12  9744  ltmul12a  11160  eluzp1m1  11924  lbzbi  11991  qreccl  12023  xrlttr  12185  elfzodifsumelfzo  12754  quoremnn0  12875  incexc2  14788  mertens  14835  ndvdsadd  15349  nn0seqcvgd  15498  isprm3  15610  isprm7  15633  pcval  15762  prdsval  16316  evlfcl  17063  frgpup1  18385  frgpup3lem  18387  ghmcmn  18434  gsumval3  18505  gsumzoppg  18541  ablfaclem2  18683  gsumdixp  18807  psrass1lem  19582  psrass1  19610  frlmgsum  20318  m2cpminvid2  20770  pmatcollpw2lem  20792  chcoeffeqlem  20900  neissex  21142  neiptopnei  21147  dissnlocfin  21543  tx1stc  21664  kqreglem1  21755  xpstopnlem1  21823  alexsublem  22058  metuel2  22580  icoopnst  22948  iocopnst  22949  volcn  23586  mbflimsup  23646  mbflim  23648  itg1addlem4  23679  itg1addlem5  23680  itg1climres  23694  limcflf  23858  dvcobr  23922  dvcnvlem  23952  dvfsumge  23998  mdegmullem  24051  plyeq0lem  24179  plypf1  24181  mtestbdd  24372  mbfulm  24373  fsumdvdscom  25124  muinv  25132  logfaclbnd  25160  logexprlim  25163  dchrinv  25199  lgsval3  25253  rpvmasum2  25414  dchrisum0lem1  25418  dchrisum0  25422  selberg  25450  selberg3lem1  25459  selberg34r  25473  pntsval2  25478  iscgrglt  25622  ercgrg  25625  legso  25707  oppperpex  25858  outpasch  25860  hpgerlem  25870  trgcopyeu  25911  dfcgra2  25934  inaghl  25944  colinearalg  26003  axeuclid  26056  axcontlem2  26058  axcontlem7  26063  wlkiswwlksupgr2  27003  grpoidinvlem4  27689  ipblnfi  28038  shmodsi  28575  eighmorth  29150  kbass5  29306  kbass6  29307  dmdmd  29486  atom1d  29539  mdsymlem2  29590  mdsymlem3  29591  mdsymlem4  29592  mdsymlem5  29593  fmptco1f1o  29760  fsumiunle  29901  2sqmo  29973  gsummpt2co  30104  suborng  30139  pstmxmet  30264  ordtconnlem1  30294  esumiun  30480  dya2iocnei  30668  omssubadd  30686  actfunsnf1o  31006  fsum2dsub  31009  reprsuc  31017  reprinfz1  31024  reprpmtf1o  31028  breprexplema  31032  circlemeth  31042  hgt750lemb  31058  resconn  31549  nosupbnd1lem5  32177  nocvxminlem  32212  uncf  33699  unccur  33703  fin2so  33707  matunitlindflem1  33716  poimirlem6  33726  poimirlem7  33727  poimirlem25  33745  poimirlem28  33748  poimirlem31  33751  poimirlem32  33752  broucube  33754  ismblfin  33761  mbfposadd  33767  itg2gt0cn  33775  ftc1anclem7  33801  ftc1anc  33803  cover2  33818  indexa  33838  filbcmb  33845  seqpo  33852  incsequz  33853  isbnd2  33891  ghomco  33999  unichnidl  34139  isfldidl  34176  dihvalc  37011  dihvalb  37015  radcnvrat  39010  reximddv3  39829  rexabslelem  40121  rexlimddv2  40526  dvnprodlem2  40639  etransclem46  40973  aacllem  43115
  Copyright terms: Public domain W3C validator