Theorem bi2anan9r 651

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  efrn2lp  5632  ltsosr  11186  seqf1olem2  14192  seqf1o  14193  pcval  17031  ltslpss  28303  uspgr2wlkeq  30235  satf0op  36232  fmlafvel  36240  fneval  37236  prtlem5  40026  prjspval  43740  rmydioph  44130  wepwsolem  44158  aomclem8  44172  sprsymrelfolem2  48683  pgnbgreunbgrlem1  49319  pgnbgreunbgrlem4  49325