Theorem cases2ALT

Alternate proof of cases2, not using dedlema or dedlemb. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 2-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \varphi \wedge \psi \vee \neg \varphi \wedge \chi \leftrightarrow (\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi) \)
Proof
l0
pm3.4
pm2.24
adantr _
l3
jca l0 _
pm2.21
l5
adantr _
pm3.4
jca l5 _
l8
jaoi l3 _
pm2.27
imdistani _
orcd _
l12
adantrr _
\( \vdash \varphi \wedge ((\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi)) \rightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \chi \)
pm2.27
imdistani _
olcd _
adantrl _
\( \vdash \neg \varphi \wedge ((\varphi \rightarrow \psi) \wedge (\neg \varphi \rightarrow \chi)) \rightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \chi \)
pm2.61ian l12 _
impbii l8 _