Theorem anabs5

Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)

Conclusion

\( \vdash \varphi \wedge (\varphi \wedge \psi) \leftrightarrow \varphi \wedge \psi \)

Proof

ibar

bicomd _

pm5.32i _