Theorem bi2anan9 635

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	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bi2an9.2	. 2 ⊢ (𝜃 → (𝜏 ↔ 𝜂))
3		pm4.38 634	. 2 ⊢ (((𝜓 ↔ 𝜒) ∧ (𝜏 ↔ 𝜂)) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
4	1, 2, 3	syl2an 595	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  bi2anan9r  636  rspc2gv  3566  2reu5  3678  ralprgf  4531  raltpg  4535  prssg  4653  prsspwg  4657  ssprss  4658  opelopab2a  5304  opelxp  5471  eqrel  5536  eqrelrel  5548  brcog  5615  tpres  6821  dff13  6869  resoprab2  7118  ovig  7143  dfoprab4f  7601  f1o2ndf1  7662  om00el  8043  oeoe  8066  eroveu  8233  endisj  8441  infxpen  9275  dfac5lem4  9387  sornom  9534  ltsrpr  10334  axcnre  10421  axmulgt0  10551  wloglei  11009  mulge0b  11347  addltmul  11710  ltxr  12349  fzadd2  12781  sumsqeq0  13380  ccat0  13762  rlim  14674  cpnnen  15403  dvds2lem  15443  opoe  15533  omoe  15534  opeo  15535  omeo  15536  gcddvds  15673  dfgcd2  15711  pcqmul  16007  xpsfrnel2  16654  eqgval  18070  frgpuplem  18613  mpfind  19991  2ndcctbss  21735  txbasval  21886  cnmpt12  21947  cnmpt22  21954  prdsxmslem2  22810  ishtpy  23247  bcthlem1  23598  bcth  23603  volun  23817  vitali  23885  itg1addlem3  23970  rolle  24258  mumullem2  25427  lgsquadlem3  25628  lgsquad  25629  2sqlem7  25670  axpasch  26398  wlkson  27108  iswwlksnon  27306  wpthswwlks2on  27415  eulplig  27941  hlimi  28644  leopadd  29588  eqrelrd2  30032  isinftm  30406  finexttrb  30611  metidv  30705  satfbrsuc  32175  gonarlem  32202  satfv0fvfmla0  32221  scutval  32819  slerec  32831  altopthg  32982  altopthbg  32983  brsegle  33123  finxpreclem3  34151  itg2addnclem3  34422  exan3  35031  exanres  35032  exanres3  35033  eqrel2  35037  brcoss  35157  brcoss3  35159  brcoels  35161  br1cossxrnres  35169  brcosscnv  35193  prtlem13  35485  dib1dim  37782  pellex  38868  ichan  43066  prsprel  43085  uspgrsprf1  43458  uspgrsprfo  43459