Theorem condan

Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.)

Hypotheses
condan.1
\( \vdash \varphi \wedge \neg \psi \rightarrow \chi \)
condan.2
\( \vdash \varphi \wedge \neg \psi \rightarrow \neg \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
condan.1
\( \vdash \varphi \wedge \neg \psi \rightarrow \chi \)
condan.2
\( \vdash \varphi \wedge \neg \psi \rightarrow \neg \chi \)
pm2.65da l0 _
notnotrd _