Theorem pm4.72

Implication in terms of biconditional and disjunction. Theorem *4.72 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jan-2013.)

Conclusion
\( \vdash \varphi \rightarrow \psi \leftrightarrow (\psi \leftrightarrow \varphi \vee \psi) \)
Proof
l0
olc
pm2.621
l2
impbid2 l0 _
l3
orc
\( \vdash \varphi \rightarrow \varphi \vee \psi \)
biimpr
\( \vdash (\psi \leftrightarrow \varphi \vee \psi) \rightarrow \varphi \vee \psi \rightarrow \psi \)
syl5 l3 _
impbii l2 _