Theorem dedlem0a

Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow (\chi \rightarrow \varphi) \rightarrow \psi \wedge \varphi) \)
Proof
l0
iba
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \psi \wedge \varphi) \)
biimt
\( \vdash (\chi \rightarrow \varphi) \rightarrow (\psi \wedge \varphi \leftrightarrow (\chi \rightarrow \varphi) \rightarrow \psi \wedge \varphi) \)
jarri _
\( \vdash \varphi \rightarrow (\psi \wedge \varphi \leftrightarrow (\chi \rightarrow \varphi) \rightarrow \psi \wedge \varphi) \)
bitrd l0 _