Theorem pm4.83

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

Conclusion
\( \vdash (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \psi) \leftrightarrow \psi \)
Proof
exmid
l1
a1bi _
\( \vdash \psi \leftrightarrow \varphi \vee \neg \varphi \rightarrow \psi \)
jaob
\( \vdash \varphi \vee \neg \varphi \rightarrow \psi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \psi) \)
bitr2i l1 _