Theorem bi2anan9 606

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  607  rspc2gv  2880  ralprg  3674  raltpg  3676  prssg  3780  prsspwg  3783  opelopab2a  4300  opelxp  4694  eqrel  4753  eqrelrel  4765  brcog  4834  dff13  5816  resoprab2  6020  ovig  6045  dfoprab4f  6252  f1o2ndf1  6287  eroveu  6686  th3qlem1  6697  th3qlem2  6698  th3q  6700  oviec  6701  endisj  6884  exmidapne  7329  dfplpq2  7423  dfmpq2  7424  ordpipqqs  7443  enq0enq  7500  mulnnnq0  7519  ltsrprg  7816  axcnre  7950  axmulgt0  8100  addltmul  9230  ltxr  9852  sumsqeq0  10712  mul0inf  11408  dvds2lem  11970  opoe  12062  omoe  12063  opeo  12064  omeo  12065  gcddvds  12140  dfgcd2  12191  pcqmul  12482  xpsfrnel2  12999  eqgval  13363  txbasval  14513  cnmpt12  14533  cnmpt22  14540  lgsquadlem3  15330  lgsquad  15331  2sqlem7  15372