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  8925  ltmul12a  9192  peano5uzti  9758  eluzp1m1  9955  lbzbi  10025  qreccl  10051  xrlttr  10207  xrltso  10208  elfzodifsumelfzo  10629  mertensabs  12320  ndvdsadd  12714  nn0seqcvgd  12835  isprm3  12912  ennnfonelemim  13364  grppropd  13871  ghmcmn  14180  gsumvalfi  14201  prdsval  14222  neissex  15315  lgsval3  16235