Theorem bi2anan9 571

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

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bi2anan9r  572  rspc2gv  2725  ralprg  3476  raltpg  3478  prssg  3577  prsspwg  3579  opelopab2a  4066  opelxp  4440  eqrel  4495  eqrelrel  4507  brcog  4571  dff13  5508  resoprab2  5699  ovig  5723  dfoprab4f  5920  f1o2ndf1  5950  eroveu  6335  th3qlem1  6346  th3qlem2  6347  th3q  6349  oviec  6350  endisj  6492  dfplpq2  6857  dfmpq2  6858  ordpipqqs  6877  enq0enq  6934  mulnnnq0  6953  ltsrprg  7237  axcnre  7360  axmulgt0  7502  addltmul  8585  ltxr  9178  sumsqeq0  9931  dvds2lem  10683  opoe  10770  omoe  10771  opeo  10772  omeo  10773  gcddvds  10830  dfgcd2  10878