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

Metamath Proof Explorer

Theorem 3anbi3d

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006)

		Ref	Expression
	Hypothesis	3anbi1d.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	Assertion	3anbi3d	$⊢ φ \to ((θ \land τ \land ψ) \leftrightarrow (θ \land τ \land χ))$

Step	Hyp	Ref	Expression
1		3anbi1d.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		biidd	$⊢ φ \to (θ \leftrightarrow θ)$
3	2 1	3anbi13d	$⊢ φ \to ((θ \land τ \land ψ) \leftrightarrow (θ \land τ \land χ))$