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

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 ⊢ ( ( 𝜃 ∧ 𝜑 ) → ( ( 𝜓 ∧ 𝜏 ) ↔ ( 𝜒 ∧ 𝜂 ) ) )