Theorem bi2anan9 608

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  609  rspc2gv  2920  ralprg  3718  raltpg  3720  prssg  3828  prsspwg  3831  ssprss  3832  opelopab2a  4357  opelxp  4753  eqrel  4813  eqrelrel  4825  brcog  4895  dff13  5904  resoprab2  6113  ovig  6138  dfoprab4f  6351  f1o2ndf1  6388  eroveu  6790  th3qlem1  6801  th3qlem2  6802  th3q  6804  oviec  6805  endisj  7003  exmidapne  7469  dfplpq2  7564  dfmpq2  7565  ordpipqqs  7584  enq0enq  7641  mulnnnq0  7660  ltsrprg  7957  axcnre  8091  axmulgt0  8241  addltmul  9371  ltxr  10000  sumsqeq0  10870  ccat0  11163  mul0inf  11792  dvds2lem  12354  opoe  12446  omoe  12447  opeo  12448  omeo  12449  gcddvds  12524  dfgcd2  12575  pcqmul  12866  xpsfrnel2  13419  eqgval  13800  txbasval  14981  cnmpt12  15001  cnmpt22  15008  lgsquadlem3  15798  lgsquad  15799  2sqlem7  15840