Theorem an32s

Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996)

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

Proof

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