Theorem
nanan
Conjunction in terms of alternative denial. (Contributed by Mario Carneiro, 9-May-2015.)
Conclusion
\( \vdash \varphi \wedge \psi \leftrightarrow \neg (\varphi \barwedge \psi) \)
Proof
df-nan
con2bii
_
This is the content in the right pane.