Theorem simpl

Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Jun-2022.)

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