Theorem anassrs 338

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 294	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp31 280	1 |- (((ph /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  anabsan2 387  bi2ralda 1232  bi2rexdva 1234  rcla42ev 1405  tfindsg2 2403  imainss 2649  f1oiso 2942  oalim 3135  omlim 3136  oaass 3163  undom 3342  sbthlem4 3352  mapenlem1 3384  mapenlem2 3385  mapdom2 3389  mapxpen 3390  mapunen 3397  aceq5 3563  ondomon 3662  ltexprlem6 3941  recexsrlem 4006  axrecex 4079  divnegt 4259  uzind2 4604  qrecclt 4646  qdivclt 4647  infxpidmlem11 4943  infmap1 4950  atcvatlem 5770  atcvat4 5775  sumdmdlem 5786

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org