Theorem bianfd

A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)

Hypothesis
bianfd.1
\( \vdash \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \psi \wedge \chi) \)
Proof
l0
bianfd.1
bianfd.1
intnanrd _
2falsed l0 _