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  3631  2reu5  3763  ralprgf  4693  ralprg  4695  raltpg  4697  prssg  4818  prsspwg  4822  ssprss  4823  intprg  4980  opelopab2a  5539  opelxp  5720  eqrel  5793  eqrelrel  5806  brcog  5876  tpres  7222  dff13  7276  cbvmpov  7529  resoprab2  7553  ovig  7580  dfoprab4f  8082  f1o2ndf1  8148  om00el  8615  oeoe  8638  eroveu  8853  endisj  9099  infxpen  10055  dfac5lem4OLD  10169  sornom  10318  ltsrpr  11118  axcnre  11205  axmulgt0  11336  wloglei  11796  mulge0b  12139  addltmul  12504  ltxr  13158  fzadd2  13600  sumsqeq0  14219  ccat0  14615  rlim  15532  cpnnen  16266  dvds2lem  16307  opoe  16401  omoe  16402  opeo  16403  omeo  16404  gcddvds  16541  dfgcd2  16584  pcqmul  16892  xpsfrnel2  17610  eqgval  19196  frgpuplem  19791  mpfind  22132  2ndcctbss  23464  txbasval  23615  cnmpt12  23676  cnmpt22  23683  prdsxmslem2  24543  ishtpy  25005  bcthlem1  25359  bcth  25364  volun  25581  vitali  25649  itg1addlem3  25734  rolle  26029  mumullem2  27224  lgsquadlem3  27427  lgsquad  27428  2sqlem7  27469  scutval  27846  slerec  27865  remulscllem2  28434  axpasch  28957  wlkson  29675  iswwlksnon  29874  wpthswwlks2on  29982  eulplig  30505  hlimi  31208  leopadd  32152  brab2d  32620  eqrelrd2  32629  cntzun  33072  isinftm  33189  finexttrb  33716  metidv  33892  satfv1  35369  satfbrsuc  35372  gonarlem  35400  satfv0fvfmla0  35419  satfv1fvfmla1  35429  altopthg  35969  altopthbg  35970  brsegle  36110  bj-imdirvallem  37182  finxpreclem3  37395  itg2addnclem3  37681  exan3  38296  exanres  38297  exanres3  38298  eqrel2  38301  brcoss  38433  brcoss3  38435  brcoels  38437  br1cossxrnres  38450  brcosscnv  38474  prtlem13  38870  dib1dim  41168  f1o2d2  42274  pellex  42851  tfsconcatb0  43362  tfsconcat00  43365  prsprel  47479  uspgrsprf1  48068  uspgrsprfo  48069  brab2ddw2  48748