Theorem anasss 397

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  anass  399  anabss3  575  wepo  4319  wetrep  4320  fvun1  5534  f1elima  5723  caovimo  6014  supisoti  6954  prarloc  7423  reapmul1  8470  ltmul12a  8731  peano5uzti  9272  eluzp1m1  9462  lbzbi  9525  qreccl  9551  xrlttr  9702  xrltso  9703  elfzodifsumelfzo  10100  mertensabs  11434  ndvdsadd  11822  nn0seqcvgd  11918  isprm3  11995  ennnfonelemim  12164  neissex  12576