Theorem cases

Case disjunction according to the value of \( \varphi \). (Contributed by NM, 25-Apr-2019.)

Hypotheses
cases.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
cases.2
\( \vdash \neg \varphi \rightarrow (\psi \leftrightarrow \theta) \)
Conclusion
\( \vdash \psi \leftrightarrow \varphi \wedge \chi \vee \neg \varphi \wedge \theta \)
Proof
exmid
l1
biantrur _
\( \vdash \psi \leftrightarrow (\varphi \vee \neg \varphi) \wedge \psi \)
l2
andir
\( \vdash (\varphi \vee \neg \varphi) \wedge \psi \leftrightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \psi \)
cases.1
l4
pm5.32i _
cases.2
pm5.32i _
orbi12i l4 _
\( \vdash \varphi \wedge \psi \vee \neg \varphi \wedge \psi \leftrightarrow \varphi \wedge \chi \vee \neg \varphi \wedge \theta \)
3bitri l1 l2 _