Theorem bi2anan9r 650

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  efrn2lp  5642  ltsosr  11074  seqf1olem2  14074  seqf1o  14075  pcval  16899  ltslpss  28101  uspgr2wlkeq  29995  satf0op  35869  fmlafvel  35877  fneval  36863  prtlem5  39634  prjspval  43335  rmydioph  43741  wepwsolem  43769  aomclem8  43788  sprsymrelfolem2  48242  pgnbgreunbgrlem1  48878  pgnbgreunbgrlem4  48884