Theorem pm4.79

Theorem *4.79 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2013.)

Conclusion
\( \vdash (\psi \rightarrow \varphi) \vee (\chi \rightarrow \varphi) \leftrightarrow \psi \wedge \chi \rightarrow \varphi \)
Proof
l0
id
id
l2
jaoa l0 _
l3
simplim
\( \vdash \neg (\psi \rightarrow \varphi) \rightarrow \psi \)
pm3.3
\( \vdash (\psi \wedge \chi \rightarrow \varphi) \rightarrow \psi \rightarrow \chi \rightarrow \varphi \)
syl5 l3 _
orrd _
impbii l2 _