Theorem jcn

Theorem joining the consequents of two premises. Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)

Conclusion

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

Proof

pm2.27

con3d _