Theorem an32s

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

	Ref	Expression
Hypothesis	an32s.1	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \chi \right)\to \theta$$
Assertion	an32s	$$⊢\left(\left(\phi \wedge \chi \right)\wedge \psi \right)\to \theta$$

Proof

Step	Hyp	Ref	Expression
1		an32s.1	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \chi \right)\to \theta$$
2		an32	$$⊢\left(\left(\phi \wedge \chi \right)\wedge \psi \right)\leftrightarrow \left(\left(\phi \wedge \psi \right)\wedge \chi \right)$$
3	2 1	sylbi	$$⊢\left(\left(\phi \wedge \chi \right)\wedge \psi \right)\to \theta$$