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  587  biadanid  618  wepo  4462  wetrep  4463  fvun1  5721  f1elima  5924  caovimo  6226  supisoti  7269  prarloc  7783  reapmul1  8834  ltmul12a  9099  peano5uzti  9649  eluzp1m1  9841  lbzbi  9911  qreccl  9937  xrlttr  10091  xrltso  10092  elfzodifsumelfzo  10509  mertensabs  12178  ndvdsadd  12572  nn0seqcvgd  12693  isprm3  12770  ennnfonelemim  13125  prdsval  13436  grppropd  13680  ghmcmn  13994  neissex  14976  lgsval3  15837  gfsumval  16809