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  2896  ralprg  3694  raltpg  3696  prssg  3801  prsspwg  3804  ssprss  3805  opelopab2a  4329  opelxp  4723  eqrel  4782  eqrelrel  4794  brcog  4863  dff13  5860  resoprab2  6065  ovig  6090  dfoprab4f  6302  f1o2ndf1  6337  eroveu  6736  th3qlem1  6747  th3qlem2  6748  th3q  6750  oviec  6751  endisj  6944  exmidapne  7407  dfplpq2  7502  dfmpq2  7503  ordpipqqs  7522  enq0enq  7579  mulnnnq0  7598  ltsrprg  7895  axcnre  8029  axmulgt0  8179  addltmul  9309  ltxr  9932  sumsqeq0  10800  ccat0  11090  mul0inf  11667  dvds2lem  12229  opoe  12321  omoe  12322  opeo  12323  omeo  12324  gcddvds  12399  dfgcd2  12450  pcqmul  12741  xpsfrnel2  13293  eqgval  13674  txbasval  14854  cnmpt12  14874  cnmpt22  14881  lgsquadlem3  15671  lgsquad  15672  2sqlem7  15713