Theorem bianabs

Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)

Hypothesis
bianabs.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \varphi \wedge \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
l0
bianabs.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \varphi \wedge \chi) \)
ibar
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \varphi \wedge \chi) \)
bitr4d l0 _