Theorem bi2anan9 645

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  bi2anan9r  646  rspc2gv  3572  2reu5  3701  ralprgf  4629  ralprg  4631  raltpg  4633  prssg  4753  prsspwg  4757  ssprss  4758  intprg  4914  opelopab2a  5480  opelxp  5657  eqrel  5730  eqrelrel  5743  brcog  5811  tpres  7149  dff13  7202  cbvmpov  7455  resoprab2  7479  ovig  7506  dfoprab4f  8002  f1o2ndf1  8065  mpof1o2d  8069  om00el  8505  oeoe  8529  eroveu  8753  endisj  8996  infxpen  9931  dfac5lem4OLD  10045  sornom  10194  ltsrpr  10995  axcnre  11082  axmulgt0  11215  wloglei  11677  mulge0b  12021  addltmul  12408  ltxr  13061  fzadd2  13508  sumsqeq0  14136  ccat0  14533  rlim  15452  cpnnen  16191  dvds2lem  16232  opoe  16327  omoe  16328  opeo  16329  omeo  16330  gcddvds  16467  dfgcd2  16510  pcqmul  16819  xpsfrnel2  17523  eqgval  19147  frgpuplem  19742  mpfind  22095  2ndcctbss  23442  txbasval  23593  cnmpt12  23654  cnmpt22  23661  prdsxmslem2  24516  ishtpy  24961  bcthlem1  25313  bcth  25318  volun  25534  vitali  25602  itg1addlem3  25687  rolle  25979  mumullem2  27165  lgsquadlem3  27367  lgsquad  27368  2sqlem7  27409  cutsval  27794  lesrec  27813  remulscllem2  28515  axpasch  29032  wlkson  29745  iswwlksnon  29943  wpthswwlks2on  30054  eulplig  30578  hlimi  31281  leopadd  32225  tpssg  32629  brab2d  32701  eqrelrd2  32712  cntzun  33164  isinftm  33266  finexttrb  33861  metidv  34088  satfv1  35606  satfbrsuc  35609  gonarlem  35637  satfv0fvfmla0  35656  satfv1fvfmla1  35666  altopthg  36210  altopthbg  36211  brsegle  36351  bj-imdirvallem  37555  finxpreclem3  37770  itg2addnclem3  38055  exan3  38682  exanres  38683  exanres3  38684  eqrel2  38687  sucmapleftuniq  38872  brcoss  38903  brcoss3  38905  brcoels  38907  br1cossxrnres  38920  brcosscnv  38944  disjimeceqim2  39187  eldisjim3  39197  prtlem13  39375  dib1dim  41672  pellex  43295  tfsconcatb0  43804  tfsconcat00  43807  prsprel  47976  uspgrsprf1  48652  uspgrsprfo  48653  brab2ddw2  49334