Theorem bi2anan9 610

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  611  rspc2gv  2922  ralprg  3720  raltpg  3722  prssg  3830  prsspwg  3833  ssprss  3834  opelopab2a  4359  opelxp  4755  eqrel  4815  eqrelrel  4827  brcog  4897  dff13  5909  resoprab2  6118  ovig  6143  dfoprab4f  6356  f1o2ndf1  6393  eroveu  6795  th3qlem1  6806  th3qlem2  6807  th3q  6809  oviec  6810  endisj  7008  exmidapne  7479  dfplpq2  7574  dfmpq2  7575  ordpipqqs  7594  enq0enq  7651  mulnnnq0  7670  ltsrprg  7967  axcnre  8101  axmulgt0  8251  addltmul  9381  ltxr  10010  sumsqeq0  10881  ccat0  11177  mul0inf  11806  dvds2lem  12369  opoe  12461  omoe  12462  opeo  12463  omeo  12464  gcddvds  12539  dfgcd2  12590  pcqmul  12881  xpsfrnel2  13434  eqgval  13815  txbasval  14997  cnmpt12  15017  cnmpt22  15024  lgsquadlem3  15814  lgsquad  15815  2sqlem7  15856