Theorem
an3
A rearrangement of conjuncts. (Contributed by Rodolfo Medina, 25-Sep-2010.)
Conclusion
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \rightarrow \varphi \wedge \theta \)
Proof
an43
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \leftrightarrow \varphi \wedge \theta \wedge (\psi \wedge \chi) \)
simplbi
_
This is the content in the right pane.