Theorem 3anibar

Remove a hypothesis from the second member of a biconditional. (Contributed by FL, 22-Jul-2008.)

Hypothesis
3anibar.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow (\theta \leftrightarrow \chi \wedge \tau) \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow (\theta \leftrightarrow \tau) \)
Proof
l0
simp3
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \chi \)
3anibar.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow (\theta \leftrightarrow \chi \wedge \tau) \)
mpbirand l0 _