Theorem pm5.6

Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.)

Conclusion
\( \vdash \varphi \wedge \neg \psi \rightarrow \chi \leftrightarrow \varphi \rightarrow \psi \vee \chi \)
Proof
l0
impexp
\( \vdash \varphi \wedge \neg \psi \rightarrow \chi \leftrightarrow \varphi \rightarrow \neg \psi \rightarrow \chi \)
df-or
imbi2i _
\( \vdash \varphi \rightarrow \psi \vee \chi \leftrightarrow \varphi \rightarrow \neg \psi \rightarrow \chi \)
bitr4i l0 _