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  5644  ltsosr  11094  seqf1olem2  14096  seqf1o  14097  pcval  16926  ltslpss  28152  uspgr2wlkeq  30053  satf0op  35906  fmlafvel  35914  fneval  36920  prtlem5  39692  prjspval  43393  rmydioph  43799  wepwsolem  43827  aomclem8  43846  sprsymrelfolem2  48300  pgnbgreunbgrlem1  48936  pgnbgreunbgrlem4  48942