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 φ ψ χ
bi3d.2 φ θ τ
bi3d.3 φ η ζ
Assertion 3orbi123d φ ψ θ η χ τ ζ

Proof

Step Hyp Ref Expression
1 bi3d.1 φ ψ χ
2 bi3d.2 φ θ τ
3 bi3d.3 φ η ζ
4 1 2 orbi12d φ ψ θ χ τ
5 4 3 orbi12d φ ψ θ η χ τ ζ
6 df-3or ψ θ η ψ θ η
7 df-3or χ τ ζ χ τ ζ
8 5 6 7 3bitr4g φ ψ θ η χ τ ζ