Theorem anass1rs 816

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

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  sossfld  5283  infunsdom  8644  creui  10604  qreccl  11284  fsumrlim  13871  fsumo1  13872  climfsum  13880  imasvscaf  15445  grppropd  16684  grpinvpropd  16729  cycsubgcl  16843  frgpup1  17425  ringrghm  17833  phlpropd  19222  mamuass  19427  iccpnfcnv  21972  mbfeqalem  22598  mbfinf  22621  mbfinfOLD  22622  mbflimsup  22623  mbflimsupOLD  22624  mbflimlem  22625  itgfsum  22784  plypf1  23166  mtest  23359  rpvmasum2  24350  isgrp2d  25963  sspival  26377  ifeqeqx  28158  ordtconlem1  28730  xrge0iifcnv  28739  incsequz  32077  equivtotbnd  32110  intidl  32262  keridl  32265  prnc  32300  cdleme50trn123  34121  dva1dim  34552  dia1dim2  34630