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	$$⊢\left(\phi \wedge \left(\psi \wedge \chi \right)\right)\to \theta$$
Assertion	ancom2s	$$⊢\left(\phi \wedge \left(\chi \wedge \psi \right)\right)\to \theta$$

Proof

Step	Hyp	Ref	Expression
1		an12s.1	$$⊢\left(\phi \wedge \left(\psi \wedge \chi \right)\right)\to \theta$$
2		pm3.22	$$⊢\left(\chi \wedge \psi \right)\to \left(\psi \wedge \chi \right)$$
3	2 1	sylan2	$$⊢\left(\phi \wedge \left(\chi \wedge \psi \right)\right)\to \theta$$