Theorem anass1rs 849

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

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  sossfld  5580  infunsdom  9036  creui  11015  qreccl  11808  fsumrlim  14543  fsumo1  14544  climfsum  14552  imasvscaf  16199  grppropd  17437  grpinvpropd  17490  cycsubgcl  17620  frgpup1  18188  ringrghm  18605  phlpropd  20000  mamuass  20208  iccpnfcnv  22743  mbfeqalem  23409  mbfinf  23432  mbflimsup  23433  mbflimlem  23434  itgfsum  23593  plypf1  23968  mtest  24158  rpvmasum2  25201  ifeqeqx  29361  ordtconnlem1  29970  xrge0iifcnv  29979  fsum2dsub  30685  incsequz  33544  equivtotbnd  33577  intidl  33828  keridl  33831  prnc  33866  cdleme50trn123  35842  dva1dim  36273  dia1dim2  36351