This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3anbi23d

Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006)

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

Step	Hyp	Ref	Expression
1		3anbi12d.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		3anbi12d.2	$⊢ φ \to (θ \leftrightarrow τ)$
3		biidd	$⊢ φ \to (η \leftrightarrow η)$
4	3 1 2	3anbi123d	$⊢ φ \to ((η \land ψ \land θ) \leftrightarrow (η \land χ \land τ))$