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  3593  2reu5  3723  ralprgf  4662  ralprg  4664  raltpg  4666  prssg  4787  prsspwg  4791  ssprss  4792  intprg  4948  opelopab2a  5521  brab2d  5524  opelxp  5699  eqrel  5772  eqrelrel  5785  brcog  5854  tpres  7207  dff13  7258  cbvmpov  7515  resoprab2  7539  ovig  7566  dfoprab4f  8060  f1o2ndf1  8124  mpof1o2d  8128  om00el  8568  oeoe  8592  eroveu  8817  endisj  9060  infxpen  10015  sornom  10277  ltsrpr  11082  axcnre  11169  axmulgt0  11304  wloglei  11766  mulge0b  12105  addltmul  12500  ltxr  13161  fzadd2  13609  sumsqeq0  14238  ccat0  14636  rlim  15575  cpnnen  16312  dvds2lem  16353  opoe  16448  omoe  16449  opeo  16450  omeo  16451  gcddvds  16588  dfgcd2  16631  pcqmul  16940  xpsfrnel2  17645  eqgval  19294  frgpuplem  19891  mpfind  22321  2ndcctbss  23668  txbasval  23819  cnmpt12  23880  cnmpt22  23887  prdsxmslem2  24742  ishtpy  25187  bcthlem1  25539  bcth  25544  volun  25760  vitali  25828  itg1addlem3  25913  rolle  26205  mumullem2  27400  lgsquadlem3  27602  lgsquad  27603  2sqlem7  27644  cutsval  28029  lesrec  28048  remulscllem2  28750  elplngid  29120  lnincplng  29122  plngcp  29124  plngrot  29128  nhpmirhp  29136  lnperpexs  29170  ragraghl  29205  tgaaddcpbllem2  29209  brprlng  29248  prlnghpg  29256  prlngmo  29264  axpasch  29351  wlkson  30067  iswwlksnon  30274  wpthswwlks2on  30385  eulplig  30913  hlimi  31616  leopadd  32560  tpssg  32959  eqrelrd2  33037  cntzun  33468  isinftm  33570  finexttrb  34124  metidv  34351  satfv1  35897  satfbrsuc  35900  gonarlem  35928  satfv0fvfmla0  35947  satfv1fvfmla1  35957  altopthg  36501  altopthbg  36502  brsegle  36642  nmuladdss  36747  bj-imdirvallem  37886  finxpreclem3  38101  itg2addnclem3  38386  exan3  39012  exanres  39013  exanres3  39014  eqrel2  39017  sucmapleftuniq  39202  brcoss  39233  brcoss3  39235  brcoels  39237  br1cossxrnres  39250  brcosscnv  39274  disjimeceqim2  39517  eldisjim3  39527  prtlem13  39705  dib1dim  42002  pellex  43640  tfsconcatb0  44149  tfsconcat00  44152  prsprel  48314  uspgrsprf1  48990  uspgrsprfo  48991  brab2ddw2  49685