Theorem dedlem0b

Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.)

Conclusion
\( \vdash \neg \varphi \rightarrow (\psi \leftrightarrow (\psi \rightarrow \varphi) \rightarrow \chi \wedge \varphi) \)
Proof
pm2.21
imim2d _
l2
com23 _
l3
pm2.21
simpr
imim12i l3 _
con1d _
com12 _
impbid l2 _