3anbi123i

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

	Ref	Expression
Hypotheses	bi3.1	$⊢ φ \leftrightarrow ψ$
	bi3.2	$⊢ χ \leftrightarrow θ$
	bi3.3	$⊢ τ \leftrightarrow η$
Assertion	3anbi123i	$⊢ (φ \land χ \land τ) \leftrightarrow (ψ \land θ \land η)$

Step	Hyp	Ref	Expression
1		bi3.1	$⊢ φ \leftrightarrow ψ$
2		bi3.2	$⊢ χ \leftrightarrow θ$
3		bi3.3	$⊢ τ \leftrightarrow η$
4	1 2	anbi12i	$⊢ (φ \land χ) \leftrightarrow (ψ \land θ)$
5	4 3	anbi12i	$⊢ ((φ \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	3bitr4i	$⊢ (φ \land χ \land τ) \leftrightarrow (ψ \land θ \land η)$

Metamath Proof Explorer