Theorem orabs

Absorption of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 28-Feb-2014.)

Conclusion
\( \vdash \varphi \leftrightarrow (\varphi \vee \psi) \wedge \varphi \)
Proof
orc
pm4.71ri _