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  9765  eluzp1m1  9962  lbzbi  10032  qreccl  10058  xrlttr  10214  xrltso  10215  elfzodifsumelfzo  10636  mertensabs  12329  ndvdsadd  12723  nn0seqcvgd  12844  isprm3  12921  ennnfonelemim  13373  grppropd  13881  ghmcmn  14221  gsumvalfi  14242  prdsval  14280  psrass1filem  15177  psrass1fi  15201  neissex  15391  lgsval3  16342