Theorem simplim

Simplification. Similar to Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 21-Jul-2012.)

Conclusion

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

Proof

pm2.21

con1i _