Metamath Proof Explorer

Theorem bi2anan9r

Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996)

Ref Expression
Hypotheses bi2an9.1 ⊢ φ → ψ ↔ χ
bi2an9.2 ⊢ θ → τ ↔ η
Assertion bi2anan9r ⊢ θ ∧ φ → ψ ∧ τ ↔ χ ∧ η

Proof

Step Hyp Ref Expression
1 bi2an9.1 ⊢ φ → ψ ↔ χ
2 bi2an9.2 ⊢ θ → τ ↔ η
3 1 2 bi2anan9 ⊢ φ ∧ θ → ψ ∧ τ ↔ χ ∧ η
4 3 ancoms ⊢ θ ∧ φ → ψ ∧ τ ↔ χ ∧ η