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  552  wepo  4186  wetrep  4187  fvun1  5370  f1elima  5552  caovimo  5838  supisoti  6703  prarloc  7060  reapmul1  8070  ltmul12a  8319  peano5uzti  8852  eluzp1m1  9040  lbzbi  9099  qreccl  9125  xrlttr  9263  xrltso  9264  elfzodifsumelfzo  9608  mertensabs  10927  ndvdsadd  11205  nn0seqcvgd  11297  isprm3  11374