Theorem anabs7

Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 17-Nov-2013.)

Conclusion

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

Proof

simpr

pm4.71ri _

bicomi _