Theorem bi2anan9 636

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 635	. 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  637  rspc2gv  3569  2reu5  3693  ralprgf  4628  ralprg  4630  raltpg  4634  prssg  4752  prsspwg  4756  ssprss  4757  intprg  4912  opelopab2a  5448  opelxp  5625  eqrel  5695  eqrelrel  5707  brcog  5775  tpres  7076  dff13  7128  resoprab2  7393  ovig  7419  dfoprab4f  7896  f1o2ndf1  7963  om00el  8407  oeoe  8430  eroveu  8601  endisj  8845  infxpen  9770  dfac5lem4  9882  sornom  10033  ltsrpr  10833  axcnre  10920  axmulgt0  11049  wloglei  11507  mulge0b  11845  addltmul  12209  ltxr  12851  fzadd2  13291  sumsqeq0  13896  ccat0  14280  rlim  15204  cpnnen  15938  dvds2lem  15978  opoe  16072  omoe  16073  opeo  16074  omeo  16075  gcddvds  16210  dfgcd2  16254  pcqmul  16554  xpsfrnel2  17275  eqgval  18805  frgpuplem  19378  mpfind  21317  2ndcctbss  22606  txbasval  22757  cnmpt12  22818  cnmpt22  22825  prdsxmslem2  23685  ishtpy  24135  bcthlem1  24488  bcth  24493  volun  24709  vitali  24777  itg1addlem3  24862  rolle  25154  mumullem2  26329  lgsquadlem3  26530  lgsquad  26531  2sqlem7  26572  axpasch  27309  wlkson  28024  iswwlksnon  28218  wpthswwlks2on  28326  eulplig  28847  hlimi  29550  leopadd  30494  eqrelrd2  30956  cntzun  31320  isinftm  31435  finexttrb  31737  metidv  31842  satfv1  33325  satfbrsuc  33328  gonarlem  33356  satfv0fvfmla0  33375  satfv1fvfmla1  33385  scutval  33994  slerec  34013  altopthg  34269  altopthbg  34270  brsegle  34410  bj-imdirvallem  35351  finxpreclem3  35564  itg2addnclem3  35830  exan3  36429  exanres  36430  exanres3  36431  eqrel2  36435  brcoss  36554  brcoss3  36556  brcoels  36558  br1cossxrnres  36566  brcosscnv  36590  prtlem13  36882  dib1dim  39179  pellex  40657  prsprel  44939  uspgrsprf1  45309  uspgrsprfo  45310