Theorem pm4.44

Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)

Conclusion
\( \vdash \varphi \leftrightarrow \varphi \vee \varphi \wedge \psi \)
Proof
l0
orc
l1
id
simpl
jaoi l1 _
impbii l0 _