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  3584  2reu5  3714  ralprgf  4649  ralprg  4651  raltpg  4653  prssg  4773  prsspwg  4777  ssprss  4778  intprg  4934  opelopab2a  5481  opelxp  5658  eqrel  5731  eqrelrel  5744  brcog  5813  tpres  7145  dff13  7198  cbvmpov  7451  resoprab2  7475  ovig  7502  dfoprab4f  7998  f1o2ndf1  8062  om00el  8501  oeoe  8525  eroveu  8747  endisj  8990  infxpen  9922  dfac5lem4OLD  10036  sornom  10185  ltsrpr  10986  axcnre  11073  axmulgt0  11205  wloglei  11667  mulge0b  12010  addltmul  12375  ltxr  13027  fzadd2  13473  sumsqeq0  14100  ccat0  14497  rlim  15416  cpnnen  16152  dvds2lem  16193  opoe  16288  omoe  16289  opeo  16290  omeo  16291  gcddvds  16428  dfgcd2  16471  pcqmul  16779  xpsfrnel2  17483  eqgval  19104  frgpuplem  19699  mpfind  22068  2ndcctbss  23397  txbasval  23548  cnmpt12  23609  cnmpt22  23616  prdsxmslem2  24471  ishtpy  24925  bcthlem1  25278  bcth  25283  volun  25500  vitali  25568  itg1addlem3  25653  rolle  25948  mumullem2  27144  lgsquadlem3  27347  lgsquad  27348  2sqlem7  27389  scutval  27768  slerec  27787  remulscllem2  28446  axpasch  28963  wlkson  29677  iswwlksnon  29875  wpthswwlks2on  29986  eulplig  30509  hlimi  31212  leopadd  32156  tpssg  32561  brab2d  32632  eqrelrd2  32643  cntzun  33110  isinftm  33212  finexttrb  33771  metidv  33998  satfv1  35506  satfbrsuc  35509  gonarlem  35537  satfv0fvfmla0  35556  satfv1fvfmla1  35566  altopthg  36110  altopthbg  36111  brsegle  36251  bj-imdirvallem  37324  finxpreclem3  37537  itg2addnclem3  37813  exan3  38432  exanres  38433  exanres3  38434  eqrel2  38437  sucmapleftuniq  38602  brcoss  38633  brcoss3  38635  brcoels  38637  br1cossxrnres  38650  brcosscnv  38674  prtlem13  39067  dib1dim  41364  f1o2d2  42431  pellex  43019  tfsconcatb0  43528  tfsconcat00  43531  prsprel  47675  uspgrsprf1  48335  uspgrsprfo  48336  brab2ddw2  49017