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  3589  2reu5  3719  ralprgf  4655  ralprg  4657  raltpg  4659  prssg  4778  prsspwg  4782  ssprss  4783  intprg  4944  opelopab2a  5513  brab2d  5516  opelxp  5691  eqrel  5765  eqrelrel  5778  brcog  5849  cnveqb  6196  tpres  7217  dff13  7268  cbvmpov  7525  resoprab2  7549  ovig  7576  dfoprab4f  8078  f1o2ndf1  8146  mpof1o2d  8150  om00el  8598  oeoe  8622  eroveu  8847  endisj  9097  infxpen  10106  sornom  10368  ltsrpr  11175  axcnre  11262  axmulgt0  11397  wloglei  11861  mulge0b  12200  addltmul  12595  ltxr  13257  fzadd2  13706  sumsqeq0  14335  ccat0  14734  rlim  15677  cpnnen  16412  dvds2lem  16453  opoe  16548  omoe  16549  opeo  16550  omeo  16551  gcddvds  16688  dfgcd2  16734  pcqmul  17046  xpsfrnel2  17751  eqgval  19404  frgpuplem  20001  mpfind  22439  2ndcctbss  23789  txbasval  23940  cnmpt12  24001  cnmpt22  24008  prdsxmslem2  24863  ishtpy  25308  bcthlem1  25660  bcth  25665  volun  25881  vitali  25949  itg1addlem3  26034  rolle  26325  mumullem2  27522  lgsquadlem3  27724  lgsquad  27725  2sqlem7  27766  cutsval  28181  lesrec  28200  remulscllem2  28902  elplngid  29275  lnincplng  29277  plngcp  29279  plngrot  29283  nhpmirhp  29291  lnperpexs  29325  ragraghl  29361  tgaaddcpbllem2  29365  brprlng  29431  prlnghpg  29439  prlngmo  29447  axpasch  29534  wlkson  30250  iswwlksnon  30457  wpthswwlks2on  30568  eulplig  31102  hlimi  31805  leopadd  32749  tpssg  33190  eqrelrd2  33267  cntzun  33696  isinftm  33798  finexttrb  34353  metidv  34580  satfv1  36252  satfbrsuc  36255  gonarlem  36283  satfv0fvfmla0  36302  satfv1fvfmla1  36312  altopthg  36865  altopthbg  36866  brsegle  37006  nmuladdss  37095  bj-imdirvallem  38247  finxpreclem3  38462  itg2addnclem3  38737  exan3  39378  exanres  39379  exanres3  39380  eqrel2  39383  sucmapleftuniq  39568  brcoss  39599  brcoss3  39601  brcoels  39603  br1cossxrnres  39616  brcosscnv  39640  disjimeceqim2  39883  eldisjim3  39893  prtlem13  40071  dib1dim  42368  pellex  43988  tfsconcatb0  44492  tfsconcat00  44495  prsprel  48714  uspgrsprf1  49390  uspgrsprfo  49391  brab2ddw2  50086