Theorem anabs1

Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)

Conclusion

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

Proof

simpl

pm4.71i _

bicomi _