Theorem bimsc1

Removal of conjunct from one side of an equivalence. (Contributed by NM, 21-Jun-1993.)

Conclusion
\( \vdash (\varphi \rightarrow \psi) \wedge (\chi \leftrightarrow \psi \wedge \varphi) \rightarrow (\chi \leftrightarrow \varphi) \)
Proof
l0
id
\( \vdash (\chi \leftrightarrow \psi \wedge \varphi) \rightarrow (\chi \leftrightarrow \psi \wedge \varphi) \)
l1
simpr
ancr
impbid2 l1 _
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \wedge \varphi \leftrightarrow \varphi) \)
sylan9bbr l0 _