# Metamath Proof Explorer

## Theorem 3anbi123i

Description: Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994)

Ref Expression
Hypotheses bi3.1 ${⊢}{\phi }↔{\psi }$
bi3.2 ${⊢}{\chi }↔{\theta }$
bi3.3 ${⊢}{\tau }↔{\eta }$
Assertion 3anbi123i ${⊢}\left({\phi }\wedge {\chi }\wedge {\tau }\right)↔\left({\psi }\wedge {\theta }\wedge {\eta }\right)$

### Proof

Step Hyp Ref Expression
1 bi3.1 ${⊢}{\phi }↔{\psi }$
2 bi3.2 ${⊢}{\chi }↔{\theta }$
3 bi3.3 ${⊢}{\tau }↔{\eta }$
4 1 2 anbi12i ${⊢}\left({\phi }\wedge {\chi }\right)↔\left({\psi }\wedge {\theta }\right)$
5 4 3 anbi12i ${⊢}\left(\left({\phi }\wedge {\chi }\right)\wedge {\tau }\right)↔\left(\left({\psi }\wedge {\theta }\right)\wedge {\eta }\right)$
6 df-3an ${⊢}\left({\phi }\wedge {\chi }\wedge {\tau }\right)↔\left(\left({\phi }\wedge {\chi }\right)\wedge {\tau }\right)$
7 df-3an ${⊢}\left({\psi }\wedge {\theta }\wedge {\eta }\right)↔\left(\left({\psi }\wedge {\theta }\right)\wedge {\eta }\right)$
8 5 6 7 3bitr4i ${⊢}\left({\phi }\wedge {\chi }\wedge {\tau }\right)↔\left({\psi }\wedge {\theta }\wedge {\eta }\right)$