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  2880  ralprg  3674  raltpg  3676  prssg  3780  prsspwg  3783  opelopab2a  4300  opelxp  4694  eqrel  4753  eqrelrel  4765  brcog  4834  dff13  5818  resoprab2  6023  ovig  6048  dfoprab4f  6260  f1o2ndf1  6295  eroveu  6694  th3qlem1  6705  th3qlem2  6706  th3q  6708  oviec  6709  endisj  6892  exmidapne  7345  dfplpq2  7440  dfmpq2  7441  ordpipqqs  7460  enq0enq  7517  mulnnnq0  7536  ltsrprg  7833  axcnre  7967  axmulgt0  8117  addltmul  9247  ltxr  9869  sumsqeq0  10729  mul0inf  11425  dvds2lem  11987  opoe  12079  omoe  12080  opeo  12081  omeo  12082  gcddvds  12157  dfgcd2  12208  pcqmul  12499  xpsfrnel2  13050  eqgval  13431  txbasval  14611  cnmpt12  14631  cnmpt22  14638  lgsquadlem3  15428  lgsquad  15429  2sqlem7  15470