Theorem efald

Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)

Hypothesis
efald.1
\( \vdash \varphi \wedge \neg \psi \rightarrow \bot \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
efald.1
inegd _
notnotrd _