Theorem anasss 403

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  anass  405  anabss3  591  biadanid  622  wepo  4506  wetrep  4507  fvun1  5772  f1elima  5982  caovimo  6286  supisoti  7356  prarloc  7876  reapmul1  8931  ltmul12a  9198  peano5uzti  9764  eluzp1m1  9961  lbzbi  10031  qreccl  10057  xrlttr  10213  xrltso  10214  elfzodifsumelfzo  10635  mertensabs  12328  ndvdsadd  12722  nn0seqcvgd  12843  isprm3  12920  ennnfonelemim  13372  grppropd  13880  ghmcmn  14220  gsumvalfi  14241  prdsval  14279  psrass1filem  15186  psrass1fi  15210  neissex  15408  lgsval3  16359