Theorem dedlema

Lemma for weak deduction theorem. See also ifptru. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)

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