Theorem
bianassc
An inference to merge two lists of conjuncts. (Contributed by Peter Mazsa, 24-Sep-2022.)
Hypothesis
bianass.1
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
Conclusion
\( \vdash \eta \wedge \varphi \leftrightarrow \psi \wedge \eta \wedge \chi \)
Proof
bianass.1
l1
bianass
_
\( \vdash \eta \wedge \varphi \leftrightarrow \eta \wedge \psi \wedge \chi \)
ancom
\( \vdash \eta \wedge \psi \leftrightarrow \psi \wedge \eta \)
bianbi
l1
_
This is the content in the right pane.