# Metamath Proof Explorer

## Theorem 3orbi123d

Description: Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-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 3orbi123d ${⊢}{\phi }\to \left(\left({\psi }\vee {\theta }\vee {\eta }\right)↔\left({\chi }\vee {\tau }\vee {\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 orbi12d ${⊢}{\phi }\to \left(\left({\psi }\vee {\theta }\right)↔\left({\chi }\vee {\tau }\right)\right)$
5 4 3 orbi12d ${⊢}{\phi }\to \left(\left(\left({\psi }\vee {\theta }\right)\vee {\eta }\right)↔\left(\left({\chi }\vee {\tau }\right)\vee {\zeta }\right)\right)$
6 df-3or ${⊢}\left({\psi }\vee {\theta }\vee {\eta }\right)↔\left(\left({\psi }\vee {\theta }\right)\vee {\eta }\right)$
7 df-3or ${⊢}\left({\chi }\vee {\tau }\vee {\zeta }\right)↔\left(\left({\chi }\vee {\tau }\right)\vee {\zeta }\right)$
8 5 6 7 3bitr4g ${⊢}{\phi }\to \left(\left({\psi }\vee {\theta }\vee {\eta }\right)↔\left({\chi }\vee {\tau }\vee {\zeta }\right)\right)$