Theorem bi2anan9 614

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 469	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜏)))
3		bi2an9.2	. . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂))
4	3	anbi2d 468	. 2 ⊢ (𝜃 → ((𝜒 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
5	2, 4	sylan9bb 466	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  615  rspc2gv  2942  ralprg  3756  raltpg  3758  prssg  3867  prsspwg  3870  ssprss  3871  opelopab2a  4402  opelxp  4799  eqrel  4859  eqrelrel  4871  brcog  4942  dff13  5964  resoprab2  6175  ovig  6200  dfoprab4f  6417  f1o2ndf1  6454  eroveu  6890  th3qlem1  6901  th3qlem2  6902  th3q  6904  oviec  6905  endisj  7112  exmidapne  7616  dfplpq2  7711  dfmpq2  7712  ordpipqqs  7731  enq0enq  7788  mulnnnq0  7807  ltsrprg  8104  axcnre  8238  axmulgt0  8387  addltmul  9521  ltxr  10156  sumsqeq0  11033  ccat0  11342  mul0inf  11985  dvds2lem  12548  opoe  12640  omoe  12641  opeo  12642  omeo  12643  gcddvds  12718  dfgcd2  12769  pcqmul  13060  xpsfrnel2  13644  eqgval  14003  txbasval  15291  cnmpt12  15311  cnmpt22  15318  lgsquadlem3  16112  lgsquad  16113  2sqlem7  16154