Theorem anasss 391

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

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 356	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 253	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  anass  393  anabss3  550  wepo  4122  wetrep  4123  fvun1  5271  f1elima  5444  caovimo  5725  supisoti  6482  prarloc  6755  reapmul1  7762  ltmul12a  8005  peano5uzti  8536  eluzp1m1  8723  lbzbi  8782  qreccl  8808  xrlttr  8946  xrltso  8947  elfzodifsumelfzo  9287  ndvdsadd  10475  nn0seqcvgd  10567  isprm3  10644