Theorem bi2anan9 614

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  bi2anan9r  615  rspc2gv  2942  ralprg  3760  raltpg  3762  prssg  3872  prsspwg  3875  ssprss  3876  opelopab2a  4407  opelxp  4804  eqrel  4864  eqrelrel  4876  brcog  4947  dff13  5974  resoprab2  6185  ovig  6210  dfoprab4f  6427  f1o2ndf1  6464  eroveu  6900  th3qlem1  6911  th3qlem2  6912  th3q  6914  oviec  6915  endisj  7122  exmidapne  7626  dfplpq2  7721  dfmpq2  7722  ordpipqqs  7741  enq0enq  7798  mulnnnq0  7817  ltsrprg  8114  axcnre  8248  axmulgt0  8397  addltmul  9546  ltxr  10187  sumsqeq0  11068  ccat0  11378  mul0inf  12023  dvds2lem  12586  opoe  12678  omoe  12679  opeo  12680  omeo  12681  gcddvds  12756  dfgcd2  12807  pcqmul  13102  xpsfrnel2  13716  eqgval  14075  txbasval  15417  cnmpt12  15437  cnmpt22  15444  lgsquadlem3  16296  lgsquad  16297  2sqlem7  16338