Theorem anass1rs 808

Description: Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.)

Hypothesis

Ref	Expression
anass1rs.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )

Assertion

Ref	Expression
anass1rs	|- ( ( ( ph /\ ch ) /\ ps ) -> th )

Proof of Theorem anass1rs

Step	Hyp	Ref	Expression
1		anass1rs.1	. . 3 |- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	anassrs 646	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	2	an32s 805	1 |- ( ( ( ph /\ ch ) /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 369

This theorem is referenced by:  sossfld  5270  infunsdom  8625  creui  10570  qreccl  11246  fsumrlim  13774  fsumo1  13775  climfsum  13783  imasvscaf  15151  grppropd  16390  grpinvpropd  16435  cycsubgcl  16549  frgpup1  17115  ringrghm  17569  phlpropd  18986  mamuass  19194  iccpnfcnv  21734  mbfeqalem  22339  mbfinf  22362  mbflimsup  22363  mbflimlem  22364  itgfsum  22523  plypf1  22899  mtest  23089  rpvmasum2  24076  isgrp2d  25637  sspival  26051  ifeqeqx  27826  ordtconlem1  28345  xrge0iifcnv  28354  incsequz  31503  equivtotbnd  31536  intidl  31688  keridl  31691  prnc  31726  cdleme50trn123  33553  dva1dim  33984  dia1dim2  34062