Theorem anass1rs 783

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

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  sossfld  5276  infunsdom  8050  creui  9951  qreccl  10550  fsumrlim  12545  fsumo1  12546  climfsum  12554  imasvscaf  13719  grppropd  14778  grpinvpropd  14821  cycsubgcl  14921  frgpup1  15362  rngrghm  15667  phlpropd  16841  iccpnfcnv  18922  mbfeqalem  19487  mbfinf  19510  mbflimsup  19511  mbflimlem  19512  itgfsum  19671  plypf1  20084  mtest  20273  rpvmasum2  21159  isgrp2d  21776  sspival  22190  ifeqeqx  23954  xrge0iifcnv  24272  incsequz  26342  equivtotbnd  26377  intidl  26529  keridl  26532  prnc  26567  mamuass  27328  cdleme50trn123  31036  dva1dim  31467  dia1dim2  31545

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

This theorem depends on definitions:  df-bi 178  df-an 361