Theorem cases2

Case disjunction according to the value of \( \varphi \). (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 28-Feb-2022.)

Conclusion
\( \vdash \varphi \wedge \psi \vee \neg \varphi \wedge \chi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi) \)
Proof
l0
pm4.83
\( \vdash (\varphi \rightarrow \psi \wedge \varphi \vee \chi \wedge \neg \varphi) \wedge (\neg \varphi \rightarrow \psi \wedge \varphi \vee \chi \wedge \neg \varphi) \leftrightarrow \psi \wedge \varphi \vee \chi \wedge \neg \varphi \)
dedlema
l2
pm5.74i _
dedlemb
pm5.74i _
l5
anbi12i l2 _
\( \vdash (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi) \leftrightarrow (\varphi \rightarrow \psi \wedge \varphi \vee \chi \wedge \neg \varphi) \wedge (\neg \varphi \rightarrow \psi \wedge \varphi \vee \chi \wedge \neg \varphi) \)
l6
ancom
ancom
orbi12i l6 _
\( \vdash \varphi \wedge \psi \vee \neg \varphi \wedge \chi \leftrightarrow \psi \wedge \varphi \vee \chi \wedge \neg \varphi \)
3bitr4ri l0 l5 _