Theorem bi2anan9 595

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 460	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜏)))
3		bi2an9.2	. . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂))
4	3	anbi2d 459	. 2 ⊢ (𝜃 → ((𝜒 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
5	2, 4	sylan9bb 457	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bi2anan9r  596  rspc2gv  2796  ralprg  3569  raltpg  3571  prssg  3672  prsspwg  3674  opelopab2a  4182  opelxp  4564  eqrel  4623  eqrelrel  4635  brcog  4701  dff13  5662  resoprab2  5861  ovig  5885  dfoprab4f  6084  f1o2ndf1  6118  eroveu  6513  th3qlem1  6524  th3qlem2  6525  th3q  6527  oviec  6528  endisj  6711  dfplpq2  7155  dfmpq2  7156  ordpipqqs  7175  enq0enq  7232  mulnnnq0  7251  ltsrprg  7548  axcnre  7682  axmulgt0  7829  addltmul  8949  ltxr  9555  sumsqeq0  10364  mul0inf  11005  dvds2lem  11494  opoe  11581  omoe  11582  opeo  11583  omeo  11584  gcddvds  11641  dfgcd2  11691  txbasval  12425  cnmpt12  12445  cnmpt22  12452