Theorem pm4.82

Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)

Conclusion
\( \vdash (\varphi \rightarrow \psi) \wedge (\varphi \rightarrow \neg \psi) \leftrightarrow \neg \varphi \)
Proof
pm2.65
l1
imp _
l2
pm2.21
pm2.21
jca l2 _
impbii l1 _