Theorem anass1rs

Description: Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011)

	Ref	Expression
Hypothesis	anass1rs.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )
Assertion	anass1rs	|- ( ( ( ph /\ ch ) /\ ps ) -> th )

Proof

Step	Hyp	Ref	Expression
1		anass1rs.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )
2	1	anassrs	|- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	2	an32s	|- ( ( ( ph /\ ch ) /\ ps ) -> th )