Theorem
biantrur
A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
Hypothesis
biantrur.1
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \leftrightarrow \varphi \wedge \psi \)
Proof
biantrur.1
biantru
_
biancomi
_
This is the content in the right pane.