Theorem pm2.21dd

A contradiction implies anything. Deduction from pm2.21. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.)

Hypotheses
pm2.21dd.1
\( \vdash \varphi \rightarrow \psi \)
pm2.21dd.2
\( \vdash \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
pm2.21dd.1
\( \vdash \varphi \rightarrow \psi \)
pm2.21dd.2
\( \vdash \varphi \rightarrow \neg \psi \)
pm2.65i l0 _
pm2.21i _