Theorem bi2anan9 650

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bi2anan9r  651  rspc2gv  3586  2reu5  3716  ralprgf  4655  ralprg  4657  raltpg  4659  prssg  4780  prsspwg  4784  ssprss  4785  intprg  4941  opelopab2a  5513  brab2d  5516  opelxp  5691  eqrel  5764  eqrelrel  5777  brcog  5847  tpres  7202  dff13  7253  cbvmpov  7510  resoprab2  7534  ovig  7561  dfoprab4f  8055  f1o2ndf1  8121  mpof1o2d  8125  om00el  8567  oeoe  8591  eroveu  8816  endisj  9066  infxpen  10039  sornom  10301  ltsrpr  11108  axcnre  11195  axmulgt0  11330  wloglei  11792  mulge0b  12131  addltmul  12526  ltxr  13188  fzadd2  13636  sumsqeq0  14265  ccat0  14663  rlim  15604  cpnnen  16339  dvds2lem  16380  opoe  16475  omoe  16476  opeo  16477  omeo  16478  gcddvds  16615  dfgcd2  16658  pcqmul  16967  xpsfrnel2  17672  eqgval  19325  frgpuplem  19922  mpfind  22360  2ndcctbss  23710  txbasval  23861  cnmpt12  23922  cnmpt22  23929  prdsxmslem2  24784  ishtpy  25229  bcthlem1  25581  bcth  25586  volun  25802  vitali  25870  itg1addlem3  25955  rolle  26246  mumullem2  27445  lgsquadlem3  27647  lgsquad  27648  2sqlem7  27689  cutsval  28074  lesrec  28093  remulscllem2  28795  elplngid  29168  lnincplng  29170  plngcp  29172  plngrot  29176  nhpmirhp  29184  lnperpexs  29218  ragraghl  29254  tgaaddcpbllem2  29258  brprlng  29324  prlnghpg  29332  prlngmo  29340  axpasch  29427  wlkson  30143  iswwlksnon  30350  wpthswwlks2on  30461  eulplig  30995  hlimi  31698  leopadd  32642  tpssg  33041  eqrelrd2  33118  cntzun  33548  isinftm  33650  finexttrb  34205  metidv  34432  satfv1  35972  satfbrsuc  35975  gonarlem  36003  satfv0fvfmla0  36022  satfv1fvfmla1  36032  altopthg  36577  altopthbg  36578  brsegle  36718  nmuladdss  36807  bj-imdirvallem  37946  finxpreclem3  38161  itg2addnclem3  38436  exan3  39062  exanres  39063  exanres3  39064  eqrel2  39067  sucmapleftuniq  39252  brcoss  39283  brcoss3  39285  brcoels  39287  br1cossxrnres  39300  brcosscnv  39324  disjimeceqim2  39567  eldisjim3  39577  prtlem13  39755  dib1dim  42052  pellex  43690  tfsconcatb0  44199  tfsconcat00  44202  prsprel  48401  uspgrsprf1  49077  uspgrsprfo  49078  brab2ddw2  49772