Theorem bi2anan9 610

Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)

Hypotheses

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

Assertion

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

Proof of Theorem bi2anan9

Step	Hyp	Ref	Expression
1		bi2an9.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	anbi1d 465	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜏)))
3		bi2an9.2	. . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂))
4	3	anbi2d 464	. 2 ⊢ (𝜃 → ((𝜒 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
5	2, 4	sylan9bb 462	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bi2anan9r  611  rspc2gv  2936  ralprg  3745  raltpg  3747  prssg  3856  prsspwg  3859  ssprss  3860  opelopab2a  4388  opelxp  4784  eqrel  4844  eqrelrel  4856  brcog  4927  dff13  5947  resoprab2  6158  ovig  6183  dfoprab4f  6400  f1o2ndf1  6437  eroveu  6873  th3qlem1  6884  th3qlem2  6885  th3q  6887  oviec  6888  endisj  7088  exmidapne  7590  dfplpq2  7685  dfmpq2  7686  ordpipqqs  7705  enq0enq  7762  mulnnnq0  7781  ltsrprg  8078  axcnre  8212  axmulgt0  8361  addltmul  9492  ltxr  10127  sumsqeq0  11004  ccat0  11309  mul0inf  11951  dvds2lem  12514  opoe  12606  omoe  12607  opeo  12608  omeo  12609  gcddvds  12684  dfgcd2  12735  pcqmul  13026  xpsfrnel2  13610  eqgval  13976  txbasval  15258  cnmpt12  15278  cnmpt22  15285  lgsquadlem3  16078  lgsquad  16079  2sqlem7  16120