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 596	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  bi2anan9r  638  rspc2gv  3590  2reu5  3719  ralprgf  4658  ralprg  4660  raltpg  4664  prssg  4784  prsspwg  4788  ssprss  4789  intprg  4947  opelopab2a  5497  opelxp  5674  eqrel  5745  eqrelrel  5758  brcog  5827  tpres  7155  dff13  7207  resoprab2  7480  ovig  7506  dfoprab4f  7993  f1o2ndf1  8059  om00el  8528  oeoe  8551  eroveu  8758  endisj  9009  infxpen  9959  dfac5lem4  10071  sornom  10222  ltsrpr  11022  axcnre  11109  axmulgt0  11238  wloglei  11696  mulge0b  12034  addltmul  12398  ltxr  13045  fzadd2  13486  sumsqeq0  14093  ccat0  14476  rlim  15389  cpnnen  16122  dvds2lem  16162  opoe  16256  omoe  16257  opeo  16258  omeo  16259  gcddvds  16394  dfgcd2  16438  pcqmul  16736  xpsfrnel2  17460  eqgval  18993  frgpuplem  19568  mpfind  21554  2ndcctbss  22843  txbasval  22994  cnmpt12  23055  cnmpt22  23062  prdsxmslem2  23922  ishtpy  24372  bcthlem1  24725  bcth  24730  volun  24946  vitali  25014  itg1addlem3  25099  rolle  25391  mumullem2  26566  lgsquadlem3  26767  lgsquad  26768  2sqlem7  26809  scutval  27182  slerec  27201  axpasch  27953  wlkson  28667  iswwlksnon  28861  wpthswwlks2on  28969  eulplig  29490  hlimi  30193  leopadd  31137  eqrelrd2  31602  cntzun  31972  isinftm  32087  finexttrb  32438  metidv  32562  satfv1  34044  satfbrsuc  34047  gonarlem  34075  satfv0fvfmla0  34094  satfv1fvfmla1  34104  altopthg  34628  altopthbg  34629  brsegle  34769  bj-imdirvallem  35724  finxpreclem3  35937  itg2addnclem3  36204  exan3  36828  exanres  36829  exanres3  36830  eqrel2  36833  brcoss  36966  brcoss3  36968  brcoels  36970  br1cossxrnres  36983  brcosscnv  37007  prtlem13  37403  dib1dim  39701  pellex  41216  tfsconcatb0  41737  tfsconcat00  41740  prsprel  45799  uspgrsprf1  46169  uspgrsprfo  46170