Theorem bi2anan9 639

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 638	. 2 ⊢ (((𝜓 ↔ 𝜒) ∧ (𝜏 ↔ 𝜂)) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
4	1, 2, 3	syl2an 597	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  640  rspc2gv  3575  2reu5  3705  ralprgf  4639  ralprg  4641  raltpg  4643  prssg  4763  prsspwg  4767  ssprss  4768  intprg  4924  opelopab2a  5484  opelxp  5661  eqrel  5734  eqrelrel  5747  brcog  5816  tpres  7150  dff13  7203  cbvmpov  7456  resoprab2  7480  ovig  7507  dfoprab4f  8003  f1o2ndf1  8066  om00el  8505  oeoe  8529  eroveu  8753  endisj  8996  infxpen  9930  dfac5lem4OLD  10044  sornom  10193  ltsrpr  10994  axcnre  11081  axmulgt0  11214  wloglei  11676  mulge0b  12020  addltmul  12407  ltxr  13060  fzadd2  13507  sumsqeq0  14135  ccat0  14532  rlim  15451  cpnnen  16190  dvds2lem  16231  opoe  16326  omoe  16327  opeo  16328  omeo  16329  gcddvds  16466  dfgcd2  16509  pcqmul  16818  xpsfrnel2  17522  eqgval  19146  frgpuplem  19741  mpfind  22106  2ndcctbss  23433  txbasval  23584  cnmpt12  23645  cnmpt22  23652  prdsxmslem2  24507  ishtpy  24952  bcthlem1  25304  bcth  25309  volun  25525  vitali  25593  itg1addlem3  25678  rolle  25970  mumullem2  27160  lgsquadlem3  27362  lgsquad  27363  2sqlem7  27404  cutsval  27789  lesrec  27808  remulscllem2  28510  axpasch  29027  wlkson  29741  iswwlksnon  29939  wpthswwlks2on  30050  eulplig  30574  hlimi  31277  leopadd  32221  tpssg  32625  brab2d  32696  eqrelrd2  32707  cntzun  33158  isinftm  33260  finexttrb  33828  metidv  34055  satfv1  35564  satfbrsuc  35567  gonarlem  35595  satfv0fvfmla0  35614  satfv1fvfmla1  35624  altopthg  36168  altopthbg  36169  brsegle  36309  bj-imdirvallem  37513  finxpreclem3  37726  itg2addnclem3  38011  exan3  38638  exanres  38639  exanres3  38640  eqrel2  38643  sucmapleftuniq  38828  brcoss  38859  brcoss3  38861  brcoels  38863  br1cossxrnres  38876  brcosscnv  38900  disjimeceqim2  39143  eldisjim3  39153  prtlem13  39331  dib1dim  41628  f1o2d2  42691  pellex  43284  tfsconcatb0  43793  tfsconcat00  43796  prsprel  47962  uspgrsprf1  48638  uspgrsprfo  48639  brab2ddw2  49320