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


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