Theorem anass1rs 798

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 641	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	2	an32s 795	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  5273  infunsdom  8371  creui  10304  qreccl  10960  fsumrlim  13256  fsumo1  13257  climfsum  13265  imasvscaf  14459  grppropd  15535  grpinvpropd  15580  cycsubgcl  15686  frgpup1  16251  rngrghm  16628  phlpropd  17925  mamuass  18147  iccpnfcnv  20357  mbfeqalem  20961  mbfinf  20984  mbflimsup  20985  mbflimlem  20986  itgfsum  21145  plypf1  21564  mtest  21753  rpvmasum2  22645  isgrp2d  23544  sspival  23958  ifeqeqx  25725  ordtconlem1  26207  xrge0iifcnv  26216  incsequz  28485  equivtotbnd  28518  intidl  28670  keridl  28673  prnc  28708  cdleme50trn123  33768  dva1dim  34199  dia1dim2  34277