Theorem simpri

Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)

Hypothesis
simpri.1
\( \vdash \varphi \wedge \psi \)
Conclusion
\( \vdash \psi \)
Proof
l0
simpri.1
\( \vdash \varphi \wedge \psi \)
simpr
\( \vdash \varphi \wedge \psi \rightarrow \psi \)
ax-mp l0 _