Theorem axin2

'Not' elimination (intuitionistic logic axiom ax-in2). (Contributed by Jim Kingdon, 21-May-2018.) (New usage is discouraged.)

Conclusion

\( \vdash \neg \varphi \rightarrow \varphi \rightarrow \psi \)

Proof

pm2.21