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  2868  ralprg  3658  raltpg  3660  prssg  3764  prsspwg  3767  opelopab2a  4283  opelxp  4674  eqrel  4733  eqrelrel  4745  brcog  4812  dff13  5790  resoprab2  5993  ovig  6018  dfoprab4f  6218  f1o2ndf1  6253  eroveu  6652  th3qlem1  6663  th3qlem2  6664  th3q  6666  oviec  6667  endisj  6850  exmidapne  7289  dfplpq2  7383  dfmpq2  7384  ordpipqqs  7403  enq0enq  7460  mulnnnq0  7479  ltsrprg  7776  axcnre  7910  axmulgt0  8059  addltmul  9185  ltxr  9805  sumsqeq0  10630  mul0inf  11281  dvds2lem  11842  opoe  11932  omoe  11933  opeo  11934  omeo  11935  gcddvds  11996  dfgcd2  12047  pcqmul  12335  xpsfrnel2  12822  eqgval  13162  txbasval  14227  cnmpt12  14247  cnmpt22  14254  2sqlem7  14929