Theorem nanbi

Biconditional in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof shortened by Wolf Lammen, 27-Jun-2020.)

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\varphi \barwedge \psi) \barwedge ((\varphi \barwedge \varphi) \barwedge (\psi \barwedge \psi)) \)
Proof
l0
dfbi3
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \neg \psi \)
l1
df-or
\( \vdash \varphi \wedge \psi \vee \neg \varphi \wedge \neg \psi \leftrightarrow \neg (\varphi \wedge \psi) \rightarrow \neg \varphi \wedge \neg \psi \)
df-nan
l3
bicomi _
l4
nannot
nannot
anbi12i l4 _
imbi12i l3 _
\( \vdash \neg (\varphi \wedge \psi) \rightarrow \neg \varphi \wedge \neg \psi \leftrightarrow \varphi \barwedge \psi \rightarrow (\varphi \barwedge \varphi) \wedge (\psi \barwedge \psi) \)
l8
3bitri l0 l1 _
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \varphi \barwedge \psi \rightarrow (\varphi \barwedge \varphi) \wedge (\psi \barwedge \psi) \)
nannan
\( \vdash (\varphi \barwedge \psi) \barwedge ((\varphi \barwedge \varphi) \barwedge (\psi \barwedge \psi)) \leftrightarrow \varphi \barwedge \psi \rightarrow (\varphi \barwedge \varphi) \wedge (\psi \barwedge \psi) \)
bitr4i l8 _