Theorem an12s

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 is combined with syl (or a variant). (Contributed by NM, 13-Mar-1996)

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

Proof

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