Disjunction distributes over the biconditional. An axiom of system DS in
Vladimir Lifschitz, "On calculational proofs" (1998),
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384.
(Contributed by NM, 8-Jan-2005.) (Proof shortened by Wolf Lammen,
4-Feb-2013.)
\( \vdash \varphi \vee (\psi \leftrightarrow \chi) \leftrightarrow (\varphi \vee \psi \leftrightarrow \varphi \vee \chi) \)
\( \vdash \neg \varphi \rightarrow (\psi \leftrightarrow \chi) \leftrightarrow (\neg \varphi \rightarrow \psi \leftrightarrow \neg \varphi \rightarrow \chi) \)
\( \vdash \varphi \vee (\psi \leftrightarrow \chi) \leftrightarrow \neg \varphi \rightarrow (\psi \leftrightarrow \chi) \)
\( \vdash \varphi \vee \psi \leftrightarrow \varphi \vee \chi \leftrightarrow (\neg \varphi \rightarrow \psi \leftrightarrow \neg \varphi \rightarrow \chi) \)