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

Theorem anasss 469
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 422 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 421 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  anass  471  anabss3  673  f1elima  6996  fnfvof  7399  oecl  8138  oaass  8163  oen0  8188  oeworde  8195  omabs  8250  oiiniseg  8973  cardinfima  9499  fpwwe2lem12  10039  ltmul12a  11472  eluzp1m1  12245  lbzbi  12313  qreccl  12345  xrlttr  12510  elfzodifsumelfzo  13085  quoremnn0  13206  incexc2  15171  mertens  15220  ndvdsadd  15737  nn0seqcvgd  15890  isprm3  16003  isprm7  16028  pcval  16157  prdsval  16704  evlfcl  17448  frgpup1  18877  frgpup3lem  18879  ghmcmn  18928  gsumval3  19003  gsumzoppg  19040  ablfaclem2  19184  gsumdixp  19335  psrass1lem  20130  psrass1  20158  frlmgsum  20889  m2cpminvid2  21336  pmatcollpw2lem  21358  chcoeffeqlem  21466  neissex  21708  neiptopnei  21713  dissnlocfin  22110  tx1stc  22231  kqreglem1  22322  xpstopnlem1  22390  alexsublem  22625  metuel2  23148  icoopnst  23520  iocopnst  23521  volcn  24186  mbflimsup  24246  mbflim  24248  itg1addlem4  24279  itg1addlem5  24280  itg1climres  24294  limcflf  24460  dvcobr  24525  dvcnvlem  24555  dvfsumge  24601  mdegmullem  24655  plyeq0lem  24783  plypf1  24785  mtestbdd  24976  mbfulm  24977  fsumdvdscom  25746  muinv  25754  logfaclbnd  25782  logexprlim  25785  dchrinv  25821  lgsval3  25875  2sqmo  25997  rpvmasum2  26072  dchrisum0lem1  26076  dchrisum0  26080  selberg  26108  selberg3lem1  26117  selberg34r  26131  pntsval2  26136  iscgrglt  26284  ercgrg  26287  legso  26369  oppperpex  26523  hpgerlem  26535  trgcopyeu  26576  dfcgra2  26600  inaghl  26615  colinearalg  26680  axeuclid  26733  axcontlem2  26735  axcontlem7  26740  wlkiswwlksupgr2  27639  grpoidinvlem4  28266  ipblnfi  28614  shmodsi  29148  eighmorth  29723  kbass5  29879  kbass6  29880  dmdmd  30059  atom1d  30112  mdsymlem2  30163  mdsymlem3  30164  mdsymlem4  30165  mdsymlem5  30166  fmptco1f1o  30362  fnpreimac  30400  fsumiunle  30529  s3f1  30607  swrdf1  30614  dfmgc2lem  30661  dfmgc2  30662  pwrssmgc  30664  gsummpt2co  30691  tocyccntz  30791  cycpmconjs  30803  suborng  30893  eqgvscpbl  30924  prmidl2  30965  idlmulssprm  30966  isprmidlc  30971  qsidomlem1  30973  qsidomlem2  30974  mxidlprm  30985  ssmxidllem  30986  lindsun  31029  lbsdiflsp0  31030  fedgmullem1  31033  fedgmul  31035  extdg1id  31061  pstmxmet  31145  ordtconnlem1  31172  esumiun  31358  dya2iocnei  31545  omssubadd  31563  actfunsnf1o  31880  fsum2dsub  31883  reprsuc  31891  reprinfz1  31898  reprpmtf1o  31902  breprexplema  31906  circlemeth  31916  hgt750lemb  31932  cusgr3cyclex  32388  resconn  32498  nosupbnd1lem5  33217  nocvxminlem  33252  pibt2  34712  uncf  34909  unccur  34913  fin2so  34917  matunitlindflem1  34926  poimirlem6  34936  poimirlem7  34937  poimirlem25  34955  poimirlem28  34958  poimirlem31  34961  poimirlem32  34962  broucube  34964  ismblfin  34971  mbfposadd  34977  itg2gt0cn  34985  ftc1anclem7  35009  ftc1anc  35011  cover2  35025  indexa  35044  filbcmb  35051  seqpo  35058  incsequz  35059  isbnd2  35094  ghomco  35202  unichnidl  35342  isfldidl  35379  dihvalc  38402  dihvalb  38406  radcnvrat  40788  reximddv3  41561  rexabslelem  41833  rexlimddv2  42243  dvnprodlem2  42367  etransclem46  42700  aacllem  45074
  Copyright terms: Public domain W3C validator