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  5509  brab2d  5512  opelxp  5687  eqrel  5760  eqrelrel  5773  brcog  5844  tpres  7207  dff13  7258  cbvmpov  7515  resoprab2  7539  ovig  7566  dfoprab4f  8067  f1o2ndf1  8133  mpof1o2d  8137  om00el  8584  oeoe  8608  eroveu  8833  endisj  9083  infxpen  10093  sornom  10355  ltsrpr  11162  axcnre  11249  axmulgt0  11384  wloglei  11848  mulge0b  12187  addltmul  12582  ltxr  13244  fzadd2  13693  sumsqeq0  14322  ccat0  14721  rlim  15662  cpnnen  16397  dvds2lem  16438  opoe  16533  omoe  16534  opeo  16535  omeo  16536  gcddvds  16673  dfgcd2  16719  pcqmul  17031  xpsfrnel2  17736  eqgval  19389  frgpuplem  19986  mpfind  22424  2ndcctbss  23774  txbasval  23925  cnmpt12  23986  cnmpt22  23993  prdsxmslem2  24848  ishtpy  25293  bcthlem1  25645  bcth  25650  volun  25866  vitali  25934  itg1addlem3  26019  rolle  26310  mumullem2  27507  lgsquadlem3  27709  lgsquad  27710  2sqlem7  27751  cutsval  28166  lesrec  28185  remulscllem2  28887  elplngid  29260  lnincplng  29262  plngcp  29264  plngrot  29268  nhpmirhp  29276  lnperpexs  29310  ragraghl  29346  tgaaddcpbllem2  29350  brprlng  29416  prlnghpg  29424  prlngmo  29432  axpasch  29519  wlkson  30235  iswwlksnon  30442  wpthswwlks2on  30553  eulplig  31087  hlimi  31790  leopadd  32734  tpssg  33133  eqrelrd2  33210  cntzun  33640  isinftm  33742  finexttrb  34297  metidv  34524  satfv1  36128  satfbrsuc  36131  gonarlem  36159  satfv0fvfmla0  36178  satfv1fvfmla1  36188  altopthg  36732  altopthbg  36733  brsegle  36873  nmuladdss  36962  bj-imdirvallem  38101  finxpreclem3  38316  itg2addnclem3  38591  exan3  39232  exanres  39233  exanres3  39234  eqrel2  39237  sucmapleftuniq  39422  brcoss  39453  brcoss3  39455  brcoels  39457  br1cossxrnres  39470  brcosscnv  39494  disjimeceqim2  39737  eldisjim3  39747  prtlem13  39925  dib1dim  42222  pellex  43841  tfsconcatb0  44345  tfsconcat00  44348  prsprel  48568  uspgrsprf1  49244  uspgrsprfo  49245  brab2ddw2  49939