Theorem pm2.21ddALT

Alternate proof of pm2.21dd. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
pm2.21ddALT.1
\( \vdash \varphi \rightarrow \psi \)
pm2.21ddALT.2
\( \vdash \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
pm2.21ddALT.1
\( \vdash \varphi \rightarrow \psi \)
pm2.21ddALT.2
pm2.21d _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
mpd l0 _