Theorem pm4.43

Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)

Conclusion
\( \vdash \varphi \leftrightarrow (\varphi \vee \psi) \wedge (\varphi \vee \neg \psi) \)
Proof
pm3.24
l1
biorfri _
\( \vdash \varphi \leftrightarrow \varphi \vee \psi \wedge \neg \psi \)
ordi
\( \vdash \varphi \vee \psi \wedge \neg \psi \leftrightarrow (\varphi \vee \psi) \wedge (\varphi \vee \neg \psi) \)
bitri l1 _