Theorem anasss 337

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

Hypothesis

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

Assertion

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

Proof of Theorem anasss

Step	Hyp	Ref	Expression
1		anasss.1	. . 3 |- (((ph /\ ps) /\ ch) -> th)
2	1	exp31 293	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp32 281	1 |- ((ph /\ (ps /\ ch)) -> th)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  tz6.12-1 2842  oecl 3140  oaass 3163  oen0 3165  mapenlem1 3384  mapxpen 3390  cardinfima 3696  distrlem4pr 3924  divdivdivt 4265  uzind 4603  uzind2 4604  uzwo 4605  qnegclt 4643  qrecclt 4646  shscl 5282  shmods 5363  spansncol 5473  dmdbr 5731  atom1d 5750  atcvat4 5775  mdsymlem2 5777  mdsymlem3 5778  mdsymlem4 5779  mdsymlem5 5780

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