Theorem biantrurd

A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypothesis
biantrud.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \psi \wedge \chi) \)
Proof
l0
biantrud.1
\( \vdash \varphi \rightarrow \psi \)
ibar
\( \vdash \psi \rightarrow (\chi \leftrightarrow \psi \wedge \chi) \)
syl l0 _