Theorem bi2anan9 606

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  607  rspc2gv  2855  ralprg  3645  raltpg  3647  prssg  3751  prsspwg  3754  opelopab2a  4267  opelxp  4658  eqrel  4717  eqrelrel  4729  brcog  4796  dff13  5771  resoprab2  5974  ovig  5998  dfoprab4f  6196  f1o2ndf1  6231  eroveu  6628  th3qlem1  6639  th3qlem2  6640  th3q  6642  oviec  6643  endisj  6826  exmidapne  7261  dfplpq2  7355  dfmpq2  7356  ordpipqqs  7375  enq0enq  7432  mulnnnq0  7451  ltsrprg  7748  axcnre  7882  axmulgt0  8031  addltmul  9157  ltxr  9777  sumsqeq0  10601  mul0inf  11251  dvds2lem  11812  opoe  11902  omoe  11903  opeo  11904  omeo  11905  gcddvds  11966  dfgcd2  12017  pcqmul  12305  xpsfrnel2  12770  eqgval  13087  txbasval  13806  cnmpt12  13826  cnmpt22  13833  2sqlem7  14507