Theorem pm2.61

Theorem *2.61 of [WhiteheadRussell] p. 107. Useful for eliminating an antecedent. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Conclusion

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

Proof

pm2.6

com12 _