Theorem bi2anan9 637

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

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

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 399

This theorem is referenced by:  bi2anan9r  638  rspc2gv  3634  2reu5  3751  ralprgf  4632  raltpg  4636  prssg  4754  prsspwg  4758  ssprss  4759  opelopab2a  5424  opelxp  5593  eqrel  5660  eqrelrel  5672  brcog  5739  tpres  6965  dff13  7015  resoprab2  7273  ovig  7298  dfoprab4f  7756  f1o2ndf1  7820  om00el  8204  oeoe  8227  eroveu  8394  endisj  8606  infxpen  9442  dfac5lem4  9554  sornom  9701  ltsrpr  10501  axcnre  10588  axmulgt0  10717  wloglei  11174  mulge0b  11512  addltmul  11876  ltxr  12513  fzadd2  12945  sumsqeq0  13545  ccat0  13931  rlim  14854  cpnnen  15584  dvds2lem  15624  opoe  15714  omoe  15715  opeo  15716  omeo  15717  gcddvds  15854  dfgcd2  15896  pcqmul  16192  xpsfrnel2  16839  eqgval  18331  frgpuplem  18900  mpfind  20322  2ndcctbss  22065  txbasval  22216  cnmpt12  22277  cnmpt22  22284  prdsxmslem2  23141  ishtpy  23578  bcthlem1  23929  bcth  23934  volun  24148  vitali  24216  itg1addlem3  24301  rolle  24589  mumullem2  25759  lgsquadlem3  25960  lgsquad  25961  2sqlem7  26002  axpasch  26729  wlkson  27440  iswwlksnon  27633  wpthswwlks2on  27742  eulplig  28264  hlimi  28967  leopadd  29911  eqrelrd2  30369  cntzun  30697  isinftm  30812  finexttrb  31054  metidv  31134  satfv1  32612  satfbrsuc  32615  gonarlem  32643  satfv0fvfmla0  32662  satfv1fvfmla1  32672  scutval  33267  slerec  33279  altopthg  33430  altopthbg  33431  brsegle  33571  bj-imdirval  34474  finxpreclem3  34676  itg2addnclem3  34947  exan3  35553  exanres  35554  exanres3  35555  eqrel2  35559  brcoss  35678  brcoss3  35680  brcoels  35682  br1cossxrnres  35690  brcosscnv  35714  prtlem13  36006  dib1dim  38303  pellex  39439  ichan  43637  prsprel  43656  uspgrsprf1  44029  uspgrsprfo  44030