Theorem bigolden

Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)

Conclusion
\( \vdash \varphi \wedge \psi \leftrightarrow \varphi \leftrightarrow (\psi \leftrightarrow \varphi \vee \psi) \)
Proof
l0
pm4.71
\( \vdash \varphi \rightarrow \psi \leftrightarrow (\varphi \leftrightarrow \varphi \wedge \psi) \)
l1
pm4.72
\( \vdash \varphi \rightarrow \psi \leftrightarrow (\psi \leftrightarrow \varphi \vee \psi) \)
bicom
\( \vdash \varphi \leftrightarrow \varphi \wedge \psi \leftrightarrow (\varphi \wedge \psi \leftrightarrow \varphi) \)
3bitr3ri l0 l1 _