# Metamath Proof Explorer

## Theorem 3orbi123i

Description: Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994)

Ref Expression
Hypotheses bi3.1 ${⊢}{\phi }↔{\psi }$
bi3.2 ${⊢}{\chi }↔{\theta }$
bi3.3 ${⊢}{\tau }↔{\eta }$
Assertion 3orbi123i ${⊢}\left({\phi }\vee {\chi }\vee {\tau }\right)↔\left({\psi }\vee {\theta }\vee {\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 orbi12i ${⊢}\left({\phi }\vee {\chi }\right)↔\left({\psi }\vee {\theta }\right)$
5 4 3 orbi12i ${⊢}\left(\left({\phi }\vee {\chi }\right)\vee {\tau }\right)↔\left(\left({\psi }\vee {\theta }\right)\vee {\eta }\right)$
6 df-3or ${⊢}\left({\phi }\vee {\chi }\vee {\tau }\right)↔\left(\left({\phi }\vee {\chi }\right)\vee {\tau }\right)$
7 df-3or ${⊢}\left({\psi }\vee {\theta }\vee {\eta }\right)↔\left(\left({\psi }\vee {\theta }\right)\vee {\eta }\right)$
8 5 6 7 3bitr4i ${⊢}\left({\phi }\vee {\chi }\vee {\tau }\right)↔\left({\psi }\vee {\theta }\vee {\eta }\right)$