Theorem bi2anan9r 636

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

Hypotheses

Ref	Expression
bi2an9.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bi2an9.2	⊢ (𝜃 → (𝜏 ↔ 𝜂))

Assertion

Ref	Expression
bi2anan9r	⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Proof of Theorem bi2anan9r

Step	Hyp	Ref	Expression
1		bi2an9.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bi2an9.2	. . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂))
3	1, 2	bi2anan9 635	. 2 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
4	3	ancoms 457	1 ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 395

This theorem is referenced by:  efrn2lp  5657  ltsosr  11091  seqf1olem2  14012  seqf1o  14013  pcval  16781  sltlpss  27638  uspgr2wlkeq  29170  satf0op  34666  fmlafvel  34674  fneval  35540  prtlem5  38033  prjspval  41647  rmydioph  42055  wepwsolem  42086  aomclem8  42105  sprsymrelfolem2  46459