Theorem
an2anr
Double commutation in conjunction. (Contributed by Peter Mazsa, 27-Jun-2019.)
Conclusion
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \leftrightarrow \psi \wedge \varphi \wedge (\theta \wedge \chi) \)
Proof
l0
ancom
ancom
anbi12i
l0
_
This is the content in the right pane.