Metamath Proof Explorer

Theorem 3anbi123d

Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994)

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

Proof

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