Theorem biantru

A wff is equivalent to its conjunction with truth. (Contributed by NM, 26-May-1993.)

Hypothesis
biantru.1
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \leftrightarrow \psi \wedge \varphi \)
Proof
l0
biantru.1
\( \vdash \varphi \)
iba
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \psi \wedge \varphi) \)
ax-mp l0 _