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 595	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  638  rspc2gv  3645  2reu5  3780  ralprgf  4717  ralprg  4719  raltpg  4723  prssg  4844  prsspwg  4848  ssprss  4849  intprg  5005  opelopab2a  5554  opelxp  5736  eqrel  5808  eqrelrel  5821  brcog  5891  tpres  7238  dff13  7292  cbvmpov  7545  resoprab2  7569  ovig  7596  dfoprab4f  8097  f1o2ndf1  8163  om00el  8632  oeoe  8655  eroveu  8870  endisj  9124  infxpen  10083  dfac5lem4OLD  10197  sornom  10346  ltsrpr  11146  axcnre  11233  axmulgt0  11364  wloglei  11822  mulge0b  12165  addltmul  12529  ltxr  13178  fzadd2  13619  sumsqeq0  14228  ccat0  14624  rlim  15541  cpnnen  16277  dvds2lem  16317  opoe  16411  omoe  16412  opeo  16413  omeo  16414  gcddvds  16549  dfgcd2  16593  pcqmul  16900  xpsfrnel2  17624  eqgval  19217  frgpuplem  19814  mpfind  22154  2ndcctbss  23484  txbasval  23635  cnmpt12  23696  cnmpt22  23703  prdsxmslem2  24563  ishtpy  25023  bcthlem1  25377  bcth  25382  volun  25599  vitali  25667  itg1addlem3  25752  rolle  26048  mumullem2  27241  lgsquadlem3  27444  lgsquad  27445  2sqlem7  27486  scutval  27863  slerec  27882  remulscllem2  28451  axpasch  28974  wlkson  29692  iswwlksnon  29886  wpthswwlks2on  29994  eulplig  30517  hlimi  31220  leopadd  32164  brab2d  32629  eqrelrd2  32638  cntzun  33044  isinftm  33161  finexttrb  33675  metidv  33838  satfv1  35331  satfbrsuc  35334  gonarlem  35362  satfv0fvfmla0  35381  satfv1fvfmla1  35391  altopthg  35931  altopthbg  35932  brsegle  36072  bj-imdirvallem  37146  finxpreclem3  37359  itg2addnclem3  37633  exan3  38250  exanres  38251  exanres3  38252  eqrel2  38255  brcoss  38387  brcoss3  38389  brcoels  38391  br1cossxrnres  38404  brcosscnv  38428  prtlem13  38824  dib1dim  41122  f1o2d2  42228  pellex  42791  tfsconcatb0  43306  tfsconcat00  43309  prsprel  47361  uspgrsprf1  47870  uspgrsprfo  47871