Theorem pm3.21

Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.)

Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \psi \wedge \varphi \)
Proof
id
expcom _