Theorem bi2anan9 639

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  bi2anan9r  640  rspc2gv  3574  2reu5  3704  ralprgf  4638  ralprg  4640  raltpg  4642  prssg  4762  prsspwg  4766  ssprss  4767  intprg  4923  opelopab2a  5490  opelxp  5667  eqrel  5740  eqrelrel  5753  brcog  5821  tpres  7156  dff13  7209  cbvmpov  7462  resoprab2  7486  ovig  7513  dfoprab4f  8009  f1o2ndf1  8072  om00el  8511  oeoe  8535  eroveu  8759  endisj  9002  infxpen  9936  dfac5lem4OLD  10050  sornom  10199  ltsrpr  11000  axcnre  11087  axmulgt0  11220  wloglei  11682  mulge0b  12026  addltmul  12413  ltxr  13066  fzadd2  13513  sumsqeq0  14141  ccat0  14538  rlim  15457  cpnnen  16196  dvds2lem  16237  opoe  16332  omoe  16333  opeo  16334  omeo  16335  gcddvds  16472  dfgcd2  16515  pcqmul  16824  xpsfrnel2  17528  eqgval  19152  frgpuplem  19747  mpfind  22093  2ndcctbss  23420  txbasval  23571  cnmpt12  23632  cnmpt22  23639  prdsxmslem2  24494  ishtpy  24939  bcthlem1  25291  bcth  25296  volun  25512  vitali  25580  itg1addlem3  25665  rolle  25957  mumullem2  27143  lgsquadlem3  27345  lgsquad  27346  2sqlem7  27387  cutsval  27772  lesrec  27791  remulscllem2  28493  axpasch  29010  wlkson  29723  iswwlksnon  29921  wpthswwlks2on  30032  eulplig  30556  hlimi  31259  leopadd  32203  tpssg  32607  brab2d  32678  eqrelrd2  32689  cntzun  33140  isinftm  33242  finexttrb  33809  metidv  34036  satfv1  35545  satfbrsuc  35548  gonarlem  35576  satfv0fvfmla0  35595  satfv1fvfmla1  35605  altopthg  36149  altopthbg  36150  brsegle  36290  bj-imdirvallem  37494  finxpreclem3  37709  itg2addnclem3  37994  exan3  38621  exanres  38622  exanres3  38623  eqrel2  38626  sucmapleftuniq  38811  brcoss  38842  brcoss3  38844  brcoels  38846  br1cossxrnres  38859  brcosscnv  38883  disjimeceqim2  39126  eldisjim3  39136  prtlem13  39314  dib1dim  41611  f1o2d2  42674  pellex  43263  tfsconcatb0  43772  tfsconcat00  43775  prsprel  47947  uspgrsprf1  48623  uspgrsprfo  48624  brab2ddw2  49305