Theorem an43

Rearrangement of 4 conjuncts. (Contributed by Rodolfo Medina, 24-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Conclusion

\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \leftrightarrow \varphi \wedge \theta \wedge (\psi \wedge \chi) \)

Proof

an42

bicomi _