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  3588  2reu5  3718  ralprgf  4653  ralprg  4655  raltpg  4657  prssg  4777  prsspwg  4781  ssprss  4782  intprg  4938  opelopab2a  5491  opelxp  5668  eqrel  5741  eqrelrel  5754  brcog  5823  tpres  7157  dff13  7210  cbvmpov  7463  resoprab2  7487  ovig  7514  dfoprab4f  8010  f1o2ndf1  8074  om00el  8513  oeoe  8537  eroveu  8761  endisj  9004  infxpen  9936  dfac5lem4OLD  10050  sornom  10199  ltsrpr  11000  axcnre  11087  axmulgt0  11219  wloglei  11681  mulge0b  12024  addltmul  12389  ltxr  13041  fzadd2  13487  sumsqeq0  14114  ccat0  14511  rlim  15430  cpnnen  16166  dvds2lem  16207  opoe  16302  omoe  16303  opeo  16304  omeo  16305  gcddvds  16442  dfgcd2  16485  pcqmul  16793  xpsfrnel2  17497  eqgval  19121  frgpuplem  19716  mpfind  22085  2ndcctbss  23414  txbasval  23565  cnmpt12  23626  cnmpt22  23633  prdsxmslem2  24488  ishtpy  24942  bcthlem1  25295  bcth  25300  volun  25517  vitali  25585  itg1addlem3  25670  rolle  25965  mumullem2  27161  lgsquadlem3  27364  lgsquad  27365  2sqlem7  27406  cutsval  27791  lesrec  27810  remulscllem2  28512  axpasch  29030  wlkson  29744  iswwlksnon  29942  wpthswwlks2on  30053  eulplig  30577  hlimi  31280  leopadd  32224  tpssg  32628  brab2d  32699  eqrelrd2  32710  cntzun  33177  isinftm  33279  finexttrb  33847  metidv  34074  satfv1  35583  satfbrsuc  35586  gonarlem  35614  satfv0fvfmla0  35633  satfv1fvfmla1  35643  altopthg  36187  altopthbg  36188  brsegle  36328  bj-imdirvallem  37439  finxpreclem3  37652  itg2addnclem3  37928  exan3  38555  exanres  38556  exanres3  38557  eqrel2  38560  sucmapleftuniq  38745  brcoss  38776  brcoss3  38778  brcoels  38780  br1cossxrnres  38793  brcosscnv  38817  disjimeceqim2  39060  eldisjim3  39070  prtlem13  39248  dib1dim  41545  f1o2d2  42609  pellex  43196  tfsconcatb0  43705  tfsconcat00  43708  prsprel  47851  uspgrsprf1  48511  uspgrsprfo  48512  brab2ddw2  49193