Theorem anasss 399

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  401  anabss3  585  biadanid  614  wepo  4424  wetrep  4425  fvun1  5668  f1elima  5865  caovimo  6163  supisoti  7138  prarloc  7651  reapmul1  8703  ltmul12a  8968  peano5uzti  9516  eluzp1m1  9707  lbzbi  9772  qreccl  9798  xrlttr  9952  xrltso  9953  elfzodifsumelfzo  10367  mertensabs  11963  ndvdsadd  12357  nn0seqcvgd  12478  isprm3  12555  ennnfonelemim  12910  prdsval  13220  grppropd  13464  ghmcmn  13778  neissex  14752  lgsval3  15610