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  7627  dfplpq2  7722  dfmpq2  7723  ordpipqqs  7742  enq0enq  7799  mulnnnq0  7818  ltsrprg  8115  axcnre  8249  axmulgt0  8398  addltmul  9547  ltxr  10188  sumsqeq0  11070  ccat0  11380  mul0inf  12026  dvds2lem  12589  opoe  12681  omoe  12682  opeo  12683  omeo  12684  gcddvds  12759  dfgcd2  12810  pcqmul  13105  xpsfrnel2  13720  eqgval  14079  txbasval  15459  cnmpt12  15479  cnmpt22  15486  lgsquadlem3  16364  lgsquad  16365  2sqlem7  16406