Theorem bi2anan9 636

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  bi2anan9r  637  rspc2gv  3630  2reu5  3764  ralprgf  4704  ralprg  4706  raltpg  4710  prssg  4831  prsspwg  4835  ssprss  4836  intprg  4994  opelopab2a  5545  opelxp  5722  eqrel  5794  eqrelrel  5807  brcog  5877  tpres  7223  dff13  7275  resoprab2  7550  ovig  7577  dfoprab4f  8078  f1o2ndf1  8144  om00el  8614  oeoe  8637  eroveu  8849  endisj  9103  infxpen  10064  dfac5lem4OLD  10178  sornom  10327  ltsrpr  11127  axcnre  11214  axmulgt0  11345  wloglei  11803  mulge0b  12146  addltmul  12510  ltxr  13159  fzadd2  13600  sumsqeq0  14208  ccat0  14605  rlim  15518  cpnnen  16252  dvds2lem  16292  opoe  16386  omoe  16387  opeo  16388  omeo  16389  gcddvds  16524  dfgcd2  16568  pcqmul  16876  xpsfrnel2  17600  eqgval  19193  frgpuplem  19792  mpfind  22144  2ndcctbss  23473  txbasval  23624  cnmpt12  23685  cnmpt22  23692  prdsxmslem2  24552  ishtpy  25012  bcthlem1  25366  bcth  25371  volun  25588  vitali  25656  itg1addlem3  25741  rolle  26036  mumullem2  27231  lgsquadlem3  27434  lgsquad  27435  2sqlem7  27476  scutval  27853  slerec  27872  remulscllem2  28375  axpasch  28898  wlkson  29616  iswwlksnon  29810  wpthswwlks2on  29918  eulplig  30441  hlimi  31144  leopadd  32088  brab2d  32553  eqrelrd2  32562  cntzun  32958  isinftm  33075  finexttrb  33582  metidv  33745  satfv1  35238  satfbrsuc  35241  gonarlem  35269  satfv0fvfmla0  35288  satfv1fvfmla1  35298  altopthg  35838  altopthbg  35839  brsegle  35979  bj-imdirvallem  36934  finxpreclem3  37147  itg2addnclem3  37421  exan3  38039  exanres  38040  exanres3  38041  eqrel2  38044  brcoss  38176  brcoss3  38178  brcoels  38180  br1cossxrnres  38193  brcosscnv  38217  prtlem13  38613  dib1dim  40911  f1o2d2  42013  pellex  42563  tfsconcatb0  43081  tfsconcat00  43084  prsprel  47129  uspgrsprf1  47605  uspgrsprfo  47606