Theorem anassrs 441

Description: Associative law for conjunction applied to antecedent (eliminates syllogism).

Hypothesis

Ref	Expression
anassrs.1	|- ((ph /\ (ps /\ ch)) -> th)

Assertion

Ref	Expression
anassrs	|- (((ph /\ ps) /\ ch) -> th)

Proof of Theorem anassrs

Step	Hyp	Ref	Expression
1		anassrs.1	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
2	1	exp32 377	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp31 362	1 |- (((ph /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  anabsan2 504  2ralbida 1669  2rexbidva 1671  sspr 2466  tfindsg2 3153  imainss 3449  funiunfv 3851  f1oiso 3889  oalim 4151  omlim 4152  oaass 4179  oarec 4180  omlimcl 4193  omass 4195  oelim2 4206  undom 4418  sbthlem4 4430  mapenlem1 4469  mapenlem2 4470  mapdom2 4474  mapxpen 4475  mapunen 4482  aceq5 4712  ondomon 4828  ltexprlem6 5119  recexsrlem 5184  recextlem2 5656  uzind3OLD 6157  qrecclt 6211  qdivclt 6212  ser1add2 6275  ser1add 6276  shftf 6288  uz11t 6364  fzrevralt 6451  seqzrn2 6488  cau5i 6854  cau5 6856  cvg2 6859  faclbnd4lem4 6888  fsumcmpndx2 6980  clm4le 7019  2climnn 7039  2climnn0 7040  climrecl 7047  climge0 7049  climmullem3 7058  climmullem5 7060  caucvglem6 7098  caucvg 7099  ser1cmp2 7113  cvgratlem1 7185  fsum0diaglem2 7192  fsum0diag4 7196  elcncf1d 7205  acdc5lem1 7433  infxpidmlem11 7505  basgen2t 7581  neips 7668  neindisj 7672  innei 7677  islp2 7688  clslp 7689  cnpco 7708  blrn3 7787  blssex 7794  isopn4 7802  metcnplem 7825  metcnp 7826  metcnp3 7835  lmbr 7866  lmnn 7873  iscau5 7878  lmsslem 7887  lmss 7888  causs 7890  lmle 7895  metelcls 7900  metcnp4 7904  xpcn 7910  cmsss 7931  grplcan 8010  nvmul0or 8212  nvcni 8266  nvlmle 8268  sspival 8331  nmosetre 8359  0lno 8382  blocni 8396  minveclem9 8484  minveclem27 8502  minveclem28 8503  htthlem7 8556  hcau2 8976  shsel3t 9194  homulclt 9602  adjsymt 9676  cnvadj 9733  lnoplt 9754  unoplint 9760  counopt 9761  lnfnlt 9771  hmoplint 9782  hmopmt 9861  nmophm 9876  lnopcon 9878  lnfncon 9905  nlelch 9909  riesz3 9910  leopmult 9979  hstlet 10067  mdsl0 10145  mdslmd1lem2 10161  atcvatlem 10220  irred 10229  atcvat4 10232  sumdmdlem 10252  cdj1 10265

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain