Theorem bianfi

A wff conjoined with falsehood is false. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)

Hypothesis
bianfi.1
\( \vdash \neg \varphi \)
Conclusion
\( \vdash \varphi \leftrightarrow \psi \wedge \varphi \)
Proof
l0
bianfi.1
bianfi.1
intnan _
2false l0 _