Theorem dfor2

Logical 'or' expressed in terms of implication only. Theorem *5.25 of [WhiteheadRussell] p. 124. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Wolf Lammen, 20-Oct-2012.)

Conclusion
\( \vdash \varphi \vee \psi \leftrightarrow (\varphi \rightarrow \psi) \rightarrow \psi \)
Proof
l0
pm2.62
pm2.68
impbii l0 _