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 ⊢ φ ∧ χ ∧ τ ↔ ψ ∧ θ ∧ η