Theorem anasss 379

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 346	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 244	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  anass  381  anabss3  519  wepo  4096  wetrep  4097  fvun1  5239  f1elima  5412  caovimo  5694  prarloc  6601  reapmul1  7586  ltmul12a  7826  peano5uzti  8346  eluzp1m1  8496  lbzbi  8551  qreccl  8576  xrlttr  8716  xrltso  8717  elfzodifsumelfzo  9057  nn0seqcvgd  9880