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  5908  resoprab2  6117  ovig  6142  dfoprab4f  6355  f1o2ndf1  6392  eroveu  6794  th3qlem1  6805  th3qlem2  6806  th3q  6808  oviec  6809  endisj  7007  exmidapne  7478  dfplpq2  7573  dfmpq2  7574  ordpipqqs  7593  enq0enq  7650  mulnnnq0  7669  ltsrprg  7966  axcnre  8100  axmulgt0  8250  addltmul  9380  ltxr  10009  sumsqeq0  10879  ccat0  11172  mul0inf  11801  dvds2lem  12363  opoe  12455  omoe  12456  opeo  12457  omeo  12458  gcddvds  12533  dfgcd2  12584  pcqmul  12875  xpsfrnel2  13428  eqgval  13809  txbasval  14990  cnmpt12  15010  cnmpt22  15017  lgsquadlem3  15807  lgsquad  15808  2sqlem7  15849