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 505  2ralbida 1677  2rexbidva 1679  sspr 2475  tfindsg2 3163  imainss 3463  funiunfv 3866  f1oiso 3904  oalim 4167  omlim 4168  oaass 4195  oarec 4196  omlimcl 4209  omass 4211  oelim2 4222  undom 4438  sbthlem4 4450  mapenlem1 4489  mapenlem2 4490  mapdom2 4494  mapxpen 4495  mapunen 4502  aceq5 4740  ondomon 4856  ltexprlem6 5147  recexsrlem 5212  recextlem2 5683  uzind3OLD 6209  qrecclt 6273  qdivclt 6274  ser1add2 6338  ser1add 6339  shftf 6351  uz11t 6432  fzrevralt 6519  seqzrn2 6556  cau5i 6917  cau5 6919  cvg2 6922  faclbnd4lem4 6951  fsumcmpndx2 7042  clm4le 7081  2climnn 7102  2climnn0 7103  climrecl 7110  climge0 7112  climmullem3 7122  climmullem5 7124  caucvglem6 7162  caucvg 7163  ser1cmp2 7177  cvgratlem1 7250  fsum0diaglem2 7257  fsum0diag4 7261  elcncf1d 7270  acdc5lem1 7491  infxpidmlem11 7562  basgen2t 7639  neips 7727  neindisj 7731  innei 7736  islp2 7747  clslp 7748  cnpco 7769  blrn3 7847  blssex 7854  isopn4 7862  metcnplem 7886  metcnp 7887  metcnp3 7896  lmbr 7928  lmnn 7935  iscau5 7941  iscaunns 7944  lmsslem 7952  lmss 7953  causs 7955  lmle 7960  metelcls 7965  metcnp4 7970  xpcn 7976  cmsss 7997  grplcan 8075  nvmul0or 8272  nvcni 8329  nvcni2 8330  nvcni3 8331  nvlmle 8333  sspival 8397  nmosetre 8427  0lno 8450  blocni 8465  minveclem9 8553  minveclem27 8571  minveclem28 8572  htthlem7 8626  hcau2 9055  shsel3t 9279  homulclt 9685  adjsymt 9759  cnvadj 9816  lnoplt 9838  unoplint 9844  counopt 9845  lnfnlt 9855  hmoplint 9866  hmopmt 9946  nmophm 9961  lnopcon 9963  lnfncon 9990  nlelch 9994  riesz3 9995  leopmult 10067  hstlet 10157  mdsl0 10237  mdslmd1lem2 10253  atcvatlem 10312  irred 10321  atcvat4 10324  sumdmdlem 10345  cdj1 10360

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