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  2922  ralprg  3720  raltpg  3722  prssg  3830  prsspwg  3833  ssprss  3834  opelopab2a  4359  opelxp  4755  eqrel  4815  eqrelrel  4827  brcog  4897  dff13  5909  resoprab2  6118  ovig  6143  dfoprab4f  6356  f1o2ndf1  6393  eroveu  6795  th3qlem1  6806  th3qlem2  6807  th3q  6809  oviec  6810  endisj  7008  exmidapne  7479  dfplpq2  7574  dfmpq2  7575  ordpipqqs  7594  enq0enq  7651  mulnnnq0  7670  ltsrprg  7967  axcnre  8101  axmulgt0  8251  addltmul  9381  ltxr  10010  sumsqeq0  10881  ccat0  11177  mul0inf  11819  dvds2lem  12382  opoe  12474  omoe  12475  opeo  12476  omeo  12477  gcddvds  12552  dfgcd2  12603  pcqmul  12894  xpsfrnel2  13447  eqgval  13828  txbasval  15010  cnmpt12  15030  cnmpt22  15037  lgsquadlem3  15827  lgsquad  15828  2sqlem7  15869