Metamath Proof Explorer

Theorem bi2anan9

Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995)

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

Proof

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