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 )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  anass  405  anabss3  591  biadanid  622  wepo  4499  wetrep  4500  fvun1  5763  f1elima  5969  caovimo  6273  supisoti  7340  prarloc  7860  reapmul1  8913  ltmul12a  9180  peano5uzti  9733  eluzp1m1  9925  lbzbi  9995  qreccl  10021  xrlttr  10176  xrltso  10177  elfzodifsumelfzo  10597  mertensabs  12282  ndvdsadd  12676  nn0seqcvgd  12797  isprm3  12874  ennnfonelemim  13293  grppropd  13799  ghmcmn  14108  gsumvalfi  14129  prdsval  14150  neissex  15189  lgsval3  16051