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  5452  infunsdom  8590  creui  10527  qreccl  11198  fsumrlim  13584  fsumo1  13585  climfsum  13593  imasvscaf  14790  grppropd  15869  grpinvpropd  15914  cycsubgcl  16022  frgpup1  16589  rngrghm  17035  phlpropd  18457  mamuass  18671  iccpnfcnv  21179  mbfeqalem  21784  mbfinf  21807  mbflimsup  21808  mbflimlem  21809  itgfsum  21968  plypf1  22344  mtest  22533  rpvmasum2  23425  isgrp2d  24913  sspival  25327  ifeqeqx  27093  ordtconlem1  27542  xrge0iifcnv  27551  incsequz  29844  equivtotbnd  29877  intidl  30029  keridl  30032  prnc  30067  cdleme50trn123  35350  dva1dim  35781  dia1dim2  35859