Metamath Proof Explorer


Theorem 3anbi123i

Description: Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994)

Ref Expression
Hypotheses bi3.1 φ ψ
bi3.2 χ θ
bi3.3 τ η
Assertion 3anbi123i φ χ τ ψ θ η

Proof

Step Hyp Ref Expression
1 bi3.1 φ ψ
2 bi3.2 χ θ
3 bi3.3 τ η
4 1 2 anbi12i φ χ ψ θ
5 4 3 anbi12i φ χ τ ψ θ η
6 df-3an φ χ τ φ χ τ
7 df-3an ψ θ η ψ θ η
8 5 6 7 3bitr4i φ χ τ ψ θ η