Theorem pm5.32

Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.)

Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \leftrightarrow (\varphi \wedge \psi \leftrightarrow \varphi \wedge \chi) \)
Proof
notbi
l1
imbi2i _
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \leftrightarrow \varphi \rightarrow (\neg \psi \leftrightarrow \neg \chi) \)
l2
pm5.74
\( \vdash \varphi \rightarrow (\neg \psi \leftrightarrow \neg \chi) \leftrightarrow (\varphi \rightarrow \neg \psi \leftrightarrow \varphi \rightarrow \neg \chi) \)
notbi
\( \vdash \varphi \rightarrow \neg \psi \leftrightarrow \varphi \rightarrow \neg \chi \leftrightarrow (\neg (\varphi \rightarrow \neg \psi) \leftrightarrow \neg (\varphi \rightarrow \neg \chi)) \)
l4
3bitri l1 l2 _
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \leftrightarrow (\neg (\varphi \rightarrow \neg \psi) \leftrightarrow \neg (\varphi \rightarrow \neg \chi)) \)
l5
df-an
df-an
bibi12i l5 _
\( \vdash \varphi \wedge \psi \leftrightarrow \varphi \wedge \chi \leftrightarrow (\neg (\varphi \rightarrow \neg \psi) \leftrightarrow \neg (\varphi \rightarrow \neg \chi)) \)
bitr4i l4 _