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  2888  ralprg  3683  raltpg  3685  prssg  3789  prsspwg  3792  opelopab2a  4310  opelxp  4704  eqrel  4763  eqrelrel  4775  brcog  4844  dff13  5836  resoprab2  6041  ovig  6066  dfoprab4f  6278  f1o2ndf1  6313  eroveu  6712  th3qlem1  6723  th3qlem2  6724  th3q  6726  oviec  6727  endisj  6918  exmidapne  7371  dfplpq2  7466  dfmpq2  7467  ordpipqqs  7486  enq0enq  7543  mulnnnq0  7562  ltsrprg  7859  axcnre  7993  axmulgt0  8143  addltmul  9273  ltxr  9896  sumsqeq0  10761  ccat0  11050  mul0inf  11523  dvds2lem  12085  opoe  12177  omoe  12178  opeo  12179  omeo  12180  gcddvds  12255  dfgcd2  12306  pcqmul  12597  xpsfrnel2  13149  eqgval  13530  txbasval  14710  cnmpt12  14730  cnmpt22  14737  lgsquadlem3  15527  lgsquad  15528  2sqlem7  15569