Theorem pm5.74

Distribution of implication over biconditional. Theorem *5.74 of [WhiteheadRussell] p. 126. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 11-Apr-2013.)

Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \leftrightarrow (\varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \chi) \)
Proof
biimp
l1
imim3i _
biimpr
imim3i _
l4
impbid l1 _
biimp
l6
pm2.86d _
biimpr
pm2.86d _
impbidd l6 _
impbii l4 _