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  2923  ralprg  3724  raltpg  3726  prssg  3835  prsspwg  3838  ssprss  3839  opelopab2a  4365  opelxp  4761  eqrel  4821  eqrelrel  4833  brcog  4903  dff13  5919  resoprab2  6128  ovig  6153  dfoprab4f  6365  f1o2ndf1  6402  eroveu  6838  th3qlem1  6849  th3qlem2  6850  th3q  6852  oviec  6853  endisj  7051  exmidapne  7522  dfplpq2  7617  dfmpq2  7618  ordpipqqs  7637  enq0enq  7694  mulnnnq0  7713  ltsrprg  8010  axcnre  8144  axmulgt0  8293  addltmul  9423  ltxr  10054  sumsqeq0  10926  ccat0  11222  mul0inf  11864  dvds2lem  12427  opoe  12519  omoe  12520  opeo  12521  omeo  12522  gcddvds  12597  dfgcd2  12648  pcqmul  12939  xpsfrnel2  13492  eqgval  13873  txbasval  15061  cnmpt12  15081  cnmpt22  15088  lgsquadlem3  15881  lgsquad  15882  2sqlem7  15923