Theorem bi2anan9 608

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  609  rspc2gv  2919  ralprg  3717  raltpg  3719  prssg  3825  prsspwg  3828  ssprss  3829  opelopab2a  4353  opelxp  4749  eqrel  4808  eqrelrel  4820  brcog  4889  dff13  5898  resoprab2  6107  ovig  6132  dfoprab4f  6345  f1o2ndf1  6380  eroveu  6781  th3qlem1  6792  th3qlem2  6793  th3q  6795  oviec  6796  endisj  6991  exmidapne  7457  dfplpq2  7552  dfmpq2  7553  ordpipqqs  7572  enq0enq  7629  mulnnnq0  7648  ltsrprg  7945  axcnre  8079  axmulgt0  8229  addltmul  9359  ltxr  9983  sumsqeq0  10852  ccat0  11144  mul0inf  11767  dvds2lem  12329  opoe  12421  omoe  12422  opeo  12423  omeo  12424  gcddvds  12499  dfgcd2  12550  pcqmul  12841  xpsfrnel2  13394  eqgval  13775  txbasval  14956  cnmpt12  14976  cnmpt22  14983  lgsquadlem3  15773  lgsquad  15774  2sqlem7  15815