Metamath Proof Explorer

Theorem anbi12d

Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 26-May-1993)

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

Step	Hyp	Ref	Expression
1		anbi12d.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		anbi12d.2	$⊢ φ \to (θ \leftrightarrow τ)$
3	1	anbi1d	$⊢ φ \to ((ψ \land θ) \leftrightarrow (χ \land θ))$
4	2	anbi2d	$⊢ φ \to ((χ \land θ) \leftrightarrow (χ \land τ))$
5	3 4	bitrd	$⊢ φ \to ((ψ \land θ) \leftrightarrow (χ \land τ))$