Theorem simpr

Elimination of a conjunct. Theorem *3.27 (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 \psi \)
Proof
id
adantl _