Theorem bi2anan9 596

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 461	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜏)))
3		bi2an9.2	. . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂))
4	3	anbi2d 460	. 2 ⊢ (𝜃 → ((𝜒 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
5	2, 4	sylan9bb 458	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  597  rspc2gv  2837  ralprg  3621  raltpg  3623  prssg  3724  prsspwg  3726  opelopab2a  4237  opelxp  4628  eqrel  4687  eqrelrel  4699  brcog  4765  dff13  5730  resoprab2  5930  ovig  5954  dfoprab4f  6153  f1o2ndf1  6187  eroveu  6583  th3qlem1  6594  th3qlem2  6595  th3q  6597  oviec  6598  endisj  6781  dfplpq2  7286  dfmpq2  7287  ordpipqqs  7306  enq0enq  7363  mulnnnq0  7382  ltsrprg  7679  axcnre  7813  axmulgt0  7961  addltmul  9084  ltxr  9702  sumsqeq0  10523  mul0inf  11168  dvds2lem  11729  opoe  11817  omoe  11818  opeo  11819  omeo  11820  gcddvds  11881  dfgcd2  11932  pcqmul  12212  txbasval  12808  cnmpt12  12828  cnmpt22  12835