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  2919  ralprg  3717  raltpg  3719  prssg  3824  prsspwg  3827  ssprss  3828  opelopab2a  4352  opelxp  4748  eqrel  4807  eqrelrel  4819  brcog  4888  dff13  5891  resoprab2  6100  ovig  6125  dfoprab4f  6337  f1o2ndf1  6372  eroveu  6771  th3qlem1  6782  th3qlem2  6783  th3q  6785  oviec  6786  endisj  6979  exmidapne  7442  dfplpq2  7537  dfmpq2  7538  ordpipqqs  7557  enq0enq  7614  mulnnnq0  7633  ltsrprg  7930  axcnre  8064  axmulgt0  8214  addltmul  9344  ltxr  9967  sumsqeq0  10835  ccat0  11126  mul0inf  11747  dvds2lem  12309  opoe  12401  omoe  12402  opeo  12403  omeo  12404  gcddvds  12479  dfgcd2  12530  pcqmul  12821  xpsfrnel2  13374  eqgval  13755  txbasval  14935  cnmpt12  14955  cnmpt22  14962  lgsquadlem3  15752  lgsquad  15753  2sqlem7  15794