Theorem pm2.21fal

If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017.)

Hypotheses
pm2.21fal.1
\( \vdash \varphi \rightarrow \psi \)
pm2.21fal.2
\( \vdash \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \varphi \rightarrow \bot \)
Proof
l0
pm2.21fal.1
\( \vdash \varphi \rightarrow \psi \)
pm2.21fal.2
\( \vdash \varphi \rightarrow \neg \psi \)
pm2.21dd l0 _