Theorem oran

Disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Conclusion
\( \vdash \varphi \vee \psi \leftrightarrow \neg (\neg \varphi \wedge \neg \psi) \)
Proof
pm4.56
con2bii _