Theorem simprd

Deduction eliminating a conjunct. (Contributed by NM, 14-May-1993.) A translation of natural deduction rule /\ ER ( /\ elimination right), see [natded]. (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis

simprd.1

\( \vdash \varphi \rightarrow \psi \wedge \chi \)

Conclusion

\( \vdash \varphi \rightarrow \chi \)

Proof

simprd.1

ancomd _

\( \vdash \varphi \rightarrow \chi \wedge \psi \)

simpld _