Theorem bi2anan9 635

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 634	. 2 ⊢ (((𝜓 ↔ 𝜒) ∧ (𝜏 ↔ 𝜂)) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))
4	1, 2, 3	syl2an 595	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  bi2anan9r  636  rspc2gv  3561  2reu5  3688  ralprgf  4625  ralprg  4627  raltpg  4631  prssg  4749  prsspwg  4753  ssprss  4754  intprg  4909  opelopab2a  5441  opelxp  5616  eqrel  5684  eqrelrel  5696  brcog  5764  tpres  7058  dff13  7109  resoprab2  7371  ovig  7397  dfoprab4f  7869  f1o2ndf1  7934  om00el  8369  oeoe  8392  eroveu  8559  endisj  8799  infxpen  9701  dfac5lem4  9813  sornom  9964  ltsrpr  10764  axcnre  10851  axmulgt0  10980  wloglei  11437  mulge0b  11775  addltmul  12139  ltxr  12780  fzadd2  13220  sumsqeq0  13824  ccat0  14208  rlim  15132  cpnnen  15866  dvds2lem  15906  opoe  16000  omoe  16001  opeo  16002  omeo  16003  gcddvds  16138  dfgcd2  16182  pcqmul  16482  xpsfrnel2  17192  eqgval  18720  frgpuplem  19293  mpfind  21227  2ndcctbss  22514  txbasval  22665  cnmpt12  22726  cnmpt22  22733  prdsxmslem2  23591  ishtpy  24041  bcthlem1  24393  bcth  24398  volun  24614  vitali  24682  itg1addlem3  24767  rolle  25059  mumullem2  26234  lgsquadlem3  26435  lgsquad  26436  2sqlem7  26477  axpasch  27212  wlkson  27926  iswwlksnon  28119  wpthswwlks2on  28227  eulplig  28748  hlimi  29451  leopadd  30395  eqrelrd2  30857  cntzun  31222  isinftm  31337  finexttrb  31639  metidv  31744  satfv1  33225  satfbrsuc  33228  gonarlem  33256  satfv0fvfmla0  33275  satfv1fvfmla1  33285  scutval  33921  slerec  33940  altopthg  34196  altopthbg  34197  brsegle  34337  bj-imdirvallem  35278  finxpreclem3  35491  itg2addnclem3  35757  exan3  36356  exanres  36357  exanres3  36358  eqrel2  36362  brcoss  36481  brcoss3  36483  brcoels  36485  br1cossxrnres  36493  brcosscnv  36517  prtlem13  36809  dib1dim  39106  pellex  40573  prsprel  44827  uspgrsprf1  45197  uspgrsprfo  45198