Theorem oranabs

Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.)

Conclusion
\( \vdash (\varphi \vee \neg \psi) \wedge \psi \leftrightarrow \varphi \wedge \psi \)
Proof
l0
biortn
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \neg \psi \vee \varphi) \)
orcom
\( \vdash \neg \psi \vee \varphi \leftrightarrow \varphi \vee \neg \psi \)
bitr2di l0 _
pm5.32ri _