Theorem simpli

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

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