Theorem dedlemb

Lemma for weak deduction theorem. See also ifpfal. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Conclusion
\( \vdash \neg \varphi \rightarrow (\chi \leftrightarrow \psi \wedge \varphi \vee \chi \wedge \neg \varphi) \)
Proof
olc
l1
expcom _
pm2.21
l3
adantld _
simpl
a1i _
jaod l3 _
impbid l1 _