Theorem ancoms

Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)

Hypothesis
ancoms.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \psi \wedge \varphi \rightarrow \chi \)
Proof
ancoms.1
expcom _
imp _