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  3616  2reu5  3746  ralprgf  4675  ralprg  4677  raltpg  4679  prssg  4800  prsspwg  4804  ssprss  4805  intprg  4962  opelopab2a  5515  opelxp  5695  eqrel  5768  eqrelrel  5781  brcog  5851  tpres  7198  dff13  7252  cbvmpov  7507  resoprab2  7531  ovig  7558  dfoprab4f  8060  f1o2ndf1  8126  om00el  8593  oeoe  8616  eroveu  8831  endisj  9077  infxpen  10033  dfac5lem4OLD  10147  sornom  10296  ltsrpr  11096  axcnre  11183  axmulgt0  11314  wloglei  11774  mulge0b  12117  addltmul  12482  ltxr  13136  fzadd2  13581  sumsqeq0  14202  ccat0  14599  rlim  15516  cpnnen  16252  dvds2lem  16293  opoe  16387  omoe  16388  opeo  16389  omeo  16390  gcddvds  16527  dfgcd2  16570  pcqmul  16878  xpsfrnel2  17583  eqgval  19165  frgpuplem  19758  mpfind  22070  2ndcctbss  23398  txbasval  23549  cnmpt12  23610  cnmpt22  23617  prdsxmslem2  24473  ishtpy  24927  bcthlem1  25281  bcth  25286  volun  25503  vitali  25571  itg1addlem3  25656  rolle  25951  mumullem2  27147  lgsquadlem3  27350  lgsquad  27351  2sqlem7  27392  scutval  27769  slerec  27788  remulscllem2  28409  axpasch  28925  wlkson  29641  iswwlksnon  29840  wpthswwlks2on  29948  eulplig  30471  hlimi  31174  leopadd  32118  tpssg  32523  brab2d  32592  eqrelrd2  32601  cntzun  33067  isinftm  33184  finexttrb  33711  metidv  33928  satfv1  35390  satfbrsuc  35393  gonarlem  35421  satfv0fvfmla0  35440  satfv1fvfmla1  35450  altopthg  35990  altopthbg  35991  brsegle  36131  bj-imdirvallem  37203  finxpreclem3  37416  itg2addnclem3  37702  exan3  38317  exanres  38318  exanres3  38319  eqrel2  38322  brcoss  38454  brcoss3  38456  brcoels  38458  br1cossxrnres  38471  brcosscnv  38495  prtlem13  38891  dib1dim  41189  f1o2d2  42251  pellex  42833  tfsconcatb0  43343  tfsconcat00  43346  prsprel  47481  uspgrsprf1  48102  uspgrsprfo  48103  brab2ddw2  48788