# Metamath Proof Explorer

## Theorem an4

Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994)

Ref Expression
Assertion an4 ${⊢}\left(\left({\phi }\wedge {\psi }\right)\wedge \left({\chi }\wedge {\theta }\right)\right)↔\left(\left({\phi }\wedge {\chi }\right)\wedge \left({\psi }\wedge {\theta }\right)\right)$

### Proof

Step Hyp Ref Expression
1 anass ${⊢}\left(\left({\phi }\wedge {\psi }\right)\wedge \left({\chi }\wedge {\theta }\right)\right)↔\left({\phi }\wedge \left({\psi }\wedge \left({\chi }\wedge {\theta }\right)\right)\right)$
2 an12 ${⊢}\left({\psi }\wedge \left({\chi }\wedge {\theta }\right)\right)↔\left({\chi }\wedge \left({\psi }\wedge {\theta }\right)\right)$
3 2 bianass ${⊢}\left({\phi }\wedge \left({\psi }\wedge \left({\chi }\wedge {\theta }\right)\right)\right)↔\left(\left({\phi }\wedge {\chi }\right)\wedge \left({\psi }\wedge {\theta }\right)\right)$
4 1 3 bitri ${⊢}\left(\left({\phi }\wedge {\psi }\right)\wedge \left({\chi }\wedge {\theta }\right)\right)↔\left(\left({\phi }\wedge {\chi }\right)\wedge \left({\psi }\wedge {\theta }\right)\right)$