Theorem bianass

An inference to merge two lists of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.)

Hypothesis
bianass.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
Conclusion
\( \vdash \eta \wedge \varphi \leftrightarrow \eta \wedge \psi \wedge \chi \)
Proof
bianass.1
l1
anbi2i _
\( \vdash \eta \wedge \varphi \leftrightarrow \eta \wedge (\psi \wedge \chi) \)
anass
\( \vdash \eta \wedge \psi \wedge \chi \leftrightarrow \eta \wedge (\psi \wedge \chi) \)
bitr4i l1 _