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  2933  ralprg  3740  raltpg  3742  prssg  3851  prsspwg  3854  ssprss  3855  opelopab2a  4383  opelxp  4779  eqrel  4839  eqrelrel  4851  brcog  4922  dff13  5941  resoprab2  6150  ovig  6175  dfoprab4f  6387  f1o2ndf1  6424  eroveu  6860  th3qlem1  6871  th3qlem2  6872  th3q  6874  oviec  6875  endisj  7075  exmidapne  7574  dfplpq2  7669  dfmpq2  7670  ordpipqqs  7689  enq0enq  7746  mulnnnq0  7765  ltsrprg  8062  axcnre  8196  axmulgt0  8345  addltmul  9475  ltxr  10108  sumsqeq0  10980  ccat0  11284  mul0inf  11926  dvds2lem  12489  opoe  12581  omoe  12582  opeo  12583  omeo  12584  gcddvds  12659  dfgcd2  12710  pcqmul  13001  xpsfrnel2  13559  eqgval  13940  txbasval  15132  cnmpt12  15152  cnmpt22  15159  lgsquadlem3  15952  lgsquad  15953  2sqlem7  15994