Theorem bi2anan9 638

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 637	. 2 ⊢ (((𝜓 ↔ 𝜒) ∧ (𝜏 ↔ 𝜂)) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
4	1, 2, 3	syl2an 596	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  bi2anan9r  639  rspc2gv  3586  2reu5  3716  ralprgf  4651  ralprg  4653  raltpg  4655  prssg  4775  prsspwg  4779  ssprss  4780  intprg  4936  opelopab2a  5483  opelxp  5660  eqrel  5733  eqrelrel  5746  brcog  5815  tpres  7147  dff13  7200  cbvmpov  7453  resoprab2  7477  ovig  7504  dfoprab4f  8000  f1o2ndf1  8064  om00el  8503  oeoe  8527  eroveu  8751  endisj  8994  infxpen  9926  dfac5lem4OLD  10040  sornom  10189  ltsrpr  10990  axcnre  11077  axmulgt0  11209  wloglei  11671  mulge0b  12014  addltmul  12379  ltxr  13031  fzadd2  13477  sumsqeq0  14104  ccat0  14501  rlim  15420  cpnnen  16156  dvds2lem  16197  opoe  16292  omoe  16293  opeo  16294  omeo  16295  gcddvds  16432  dfgcd2  16475  pcqmul  16783  xpsfrnel2  17487  eqgval  19108  frgpuplem  19703  mpfind  22072  2ndcctbss  23401  txbasval  23552  cnmpt12  23613  cnmpt22  23620  prdsxmslem2  24475  ishtpy  24929  bcthlem1  25282  bcth  25287  volun  25504  vitali  25572  itg1addlem3  25657  rolle  25952  mumullem2  27148  lgsquadlem3  27351  lgsquad  27352  2sqlem7  27393  cutsval  27778  lesrec  27797  remulscllem2  28499  axpasch  29016  wlkson  29730  iswwlksnon  29928  wpthswwlks2on  30039  eulplig  30562  hlimi  31265  leopadd  32209  tpssg  32614  brab2d  32685  eqrelrd2  32696  cntzun  33163  isinftm  33265  finexttrb  33824  metidv  34051  satfv1  35559  satfbrsuc  35562  gonarlem  35590  satfv0fvfmla0  35609  satfv1fvfmla1  35619  altopthg  36163  altopthbg  36164  brsegle  36304  bj-imdirvallem  37387  finxpreclem3  37600  itg2addnclem3  37876  exan3  38498  exanres  38499  exanres3  38500  eqrel2  38503  sucmapleftuniq  38685  brcoss  38716  brcoss3  38718  brcoels  38720  br1cossxrnres  38733  brcosscnv  38757  prtlem13  39150  dib1dim  41447  f1o2d2  42511  pellex  43098  tfsconcatb0  43607  tfsconcat00  43610  prsprel  47754  uspgrsprf1  48414  uspgrsprfo  48415  brab2ddw2  49096