Theorem ancom2s

Description: Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006) (Proof shortened by Wolf Lammen, 24-Nov-2012)

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

Proof

Step	Hyp	Ref	Expression
1		an12s.1	|- ( ( ph /\ ( ps /\ ch ) ) -> th )
2		pm3.22	|- ( ( ch /\ ps ) -> ( ps /\ ch ) )
3	2 1	sylan2	|- ( ( ph /\ ( ch /\ ps ) ) -> th )