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  5280  infunsdom  8375  creui  10309  qreccl  10965  fsumrlim  13266  fsumo1  13267  climfsum  13275  imasvscaf  14469  grppropd  15547  grpinvpropd  15592  cycsubgcl  15698  frgpup1  16263  rngrghm  16682  phlpropd  18059  mamuass  18281  iccpnfcnv  20491  mbfeqalem  21095  mbfinf  21118  mbflimsup  21119  mbflimlem  21120  itgfsum  21279  plypf1  21655  mtest  21844  rpvmasum2  22736  isgrp2d  23673  sspival  24087  ifeqeqx  25853  ordtconlem1  26306  xrge0iifcnv  26315  incsequz  28597  equivtotbnd  28630  intidl  28782  keridl  28785  prnc  28820  cdleme50trn123  34038  dva1dim  34469  dia1dim2  34547