Theorem biantrud

A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)

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