Theorem anass1rs 805

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 648	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	2	an32s 802	1 |- ( ( ( ph /\ ch ) /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 369

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 371

This theorem is referenced by:  sossfld  5386  infunsdom  8487  creui  10421  qreccl  11077  fsumrlim  13385  fsumo1  13386  climfsum  13394  imasvscaf  14588  grppropd  15667  grpinvpropd  15712  cycsubgcl  15818  frgpup1  16385  rngrghm  16809  phlpropd  18202  mamuass  18424  iccpnfcnv  20641  mbfeqalem  21246  mbfinf  21269  mbflimsup  21270  mbflimlem  21271  itgfsum  21430  plypf1  21806  mtest  21995  rpvmasum2  22887  isgrp2d  23867  sspival  24281  ifeqeqx  26047  ordtconlem1  26492  xrge0iifcnv  26501  incsequz  28785  equivtotbnd  28818  intidl  28970  keridl  28973  prnc  29008  cdleme50trn123  34507  dva1dim  34938  dia1dim2  35016