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  4504  wetrep  4505  fvun1  5769  f1elima  5979  caovimo  6283  supisoti  7350  prarloc  7870  reapmul1  8923  ltmul12a  9190  peano5uzti  9754  eluzp1m1  9946  lbzbi  10016  qreccl  10042  xrlttr  10197  xrltso  10198  elfzodifsumelfzo  10619  mertensabs  12304  ndvdsadd  12698  nn0seqcvgd  12819  isprm3  12896  ennnfonelemim  13315  grppropd  13822  ghmcmn  14131  gsumvalfi  14152  prdsval  14173  neissex  15266  lgsval3  16137