Theorem bi2anan9r 637

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 636	. 2 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
4	3	ancoms 459	1 ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

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

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 397

This theorem is referenced by:  efrn2lp  5571  ltsosr  10850  seqf1olem2  13763  seqf1o  13764  pcval  16545  uspgr2wlkeq  28013  satf0op  33339  fmlafvel  33347  sltlpss  34087  fneval  34541  prtlem5  36874  prjspval  40442  rmydioph  40836  wepwsolem  40867  aomclem8  40886  sprsymrelfolem2  44945