Theorem bi2anan9 638

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 637	. 2 ⊢ (((𝜓 ↔ 𝜒) ∧ (𝜏 ↔ 𝜂)) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
4	1, 2, 3	syl2an 596	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  639  rspc2gv  3598  2reu5  3729  ralprgf  4658  ralprg  4660  raltpg  4662  prssg  4783  prsspwg  4787  ssprss  4788  intprg  4945  opelopab2a  5495  opelxp  5674  eqrel  5747  eqrelrel  5760  brcog  5830  tpres  7175  dff13  7229  cbvmpov  7484  resoprab2  7508  ovig  7535  dfoprab4f  8035  f1o2ndf1  8101  om00el  8540  oeoe  8563  eroveu  8785  endisj  9028  infxpen  9967  dfac5lem4OLD  10081  sornom  10230  ltsrpr  11030  axcnre  11117  axmulgt0  11248  wloglei  11710  mulge0b  12053  addltmul  12418  ltxr  13075  fzadd2  13520  sumsqeq0  14144  ccat0  14541  rlim  15461  cpnnen  16197  dvds2lem  16238  opoe  16333  omoe  16334  opeo  16335  omeo  16336  gcddvds  16473  dfgcd2  16516  pcqmul  16824  xpsfrnel2  17527  eqgval  19109  frgpuplem  19702  mpfind  22014  2ndcctbss  23342  txbasval  23493  cnmpt12  23554  cnmpt22  23561  prdsxmslem2  24417  ishtpy  24871  bcthlem1  25224  bcth  25229  volun  25446  vitali  25514  itg1addlem3  25599  rolle  25894  mumullem2  27090  lgsquadlem3  27293  lgsquad  27294  2sqlem7  27335  scutval  27712  slerec  27731  remulscllem2  28352  axpasch  28868  wlkson  29584  iswwlksnon  29783  wpthswwlks2on  29891  eulplig  30414  hlimi  31117  leopadd  32061  tpssg  32466  brab2d  32535  eqrelrd2  32544  cntzun  33008  isinftm  33135  finexttrb  33660  metidv  33882  satfv1  35350  satfbrsuc  35353  gonarlem  35381  satfv0fvfmla0  35400  satfv1fvfmla1  35410  altopthg  35955  altopthbg  35956  brsegle  36096  bj-imdirvallem  37168  finxpreclem3  37381  itg2addnclem3  37667  exan3  38282  exanres  38283  exanres3  38284  eqrel2  38287  brcoss  38422  brcoss3  38424  brcoels  38426  br1cossxrnres  38439  brcosscnv  38463  prtlem13  38861  dib1dim  41159  f1o2d2  42221  pellex  42823  tfsconcatb0  43333  tfsconcat00  43336  prsprel  47488  uspgrsprf1  48135  uspgrsprfo  48136  brab2ddw2  48818