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

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

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 398

This theorem is referenced by:  bi2anan9r  639  rspc2gv  3622  2reu5  3755  ralprgf  4697  ralprg  4699  raltpg  4703  prssg  4823  prsspwg  4827  ssprss  4828  intprg  4986  opelopab2a  5536  opelxp  5713  eqrel  5785  eqrelrel  5798  brcog  5867  tpres  7202  dff13  7254  resoprab2  7527  ovig  7554  dfoprab4f  8042  f1o2ndf1  8108  om00el  8576  oeoe  8599  eroveu  8806  endisj  9058  infxpen  10009  dfac5lem4  10121  sornom  10272  ltsrpr  11072  axcnre  11159  axmulgt0  11288  wloglei  11746  mulge0b  12084  addltmul  12448  ltxr  13095  fzadd2  13536  sumsqeq0  14143  ccat0  14526  rlim  15439  cpnnen  16172  dvds2lem  16212  opoe  16306  omoe  16307  opeo  16308  omeo  16309  gcddvds  16444  dfgcd2  16488  pcqmul  16786  xpsfrnel2  17510  eqgval  19057  frgpuplem  19640  mpfind  21670  2ndcctbss  22959  txbasval  23110  cnmpt12  23171  cnmpt22  23178  prdsxmslem2  24038  ishtpy  24488  bcthlem1  24841  bcth  24846  volun  25062  vitali  25130  itg1addlem3  25215  rolle  25507  mumullem2  26684  lgsquadlem3  26885  lgsquad  26886  2sqlem7  26927  scutval  27301  slerec  27320  axpasch  28199  wlkson  28913  iswwlksnon  29107  wpthswwlks2on  29215  eulplig  29738  hlimi  30441  leopadd  31385  eqrelrd2  31845  cntzun  32212  isinftm  32327  finexttrb  32741  metidv  32872  satfv1  34354  satfbrsuc  34357  gonarlem  34385  satfv0fvfmla0  34404  satfv1fvfmla1  34414  altopthg  34939  altopthbg  34940  brsegle  35080  bj-imdirvallem  36061  finxpreclem3  36274  itg2addnclem3  36541  exan3  37163  exanres  37164  exanres3  37165  eqrel2  37168  brcoss  37301  brcoss3  37303  brcoels  37305  br1cossxrnres  37318  brcosscnv  37342  prtlem13  37738  dib1dim  40036  f1o2d2  41055  pellex  41573  tfsconcatb0  42094  tfsconcat00  42097  prsprel  46155  uspgrsprf1  46525  uspgrsprfo  46526