3anbi123d

Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994)

	Ref	Expression
Hypotheses	bi3d.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	bi3d.2	$⊢ φ \to (θ \leftrightarrow τ)$
	bi3d.3	$⊢ φ \to (η \leftrightarrow ζ)$
Assertion	3anbi123d	$⊢ φ \to ((ψ \land θ \land η) \leftrightarrow (χ \land τ \land ζ))$

Step	Hyp	Ref	Expression
1		bi3d.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		bi3d.2	$⊢ φ \to (θ \leftrightarrow τ)$
3		bi3d.3	$⊢ φ \to (η \leftrightarrow ζ)$
4	1 2	anbi12d	$⊢ φ \to ((ψ \land θ) \leftrightarrow (χ \land τ))$
5	4 3	anbi12d	$⊢ φ \to (((ψ \land θ) \land η) \leftrightarrow ((χ \land τ) \land ζ))$
6		df-3an	$⊢ (ψ \land θ \land η) \leftrightarrow ((ψ \land θ) \land η)$
7		df-3an	$⊢ (χ \land τ \land ζ) \leftrightarrow ((χ \land τ) \land ζ)$
8	5 6 7	3bitr4g	$⊢ φ \to ((ψ \land θ \land η) \leftrightarrow (χ \land τ \land ζ))$

Metamath Proof Explorer