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  3632  2reu5  3767  ralprgf  4699  ralprg  4701  raltpg  4703  prssg  4824  prsspwg  4828  ssprss  4829  intprg  4986  opelopab2a  5545  opelxp  5725  eqrel  5797  eqrelrel  5810  brcog  5880  tpres  7221  dff13  7275  cbvmpov  7528  resoprab2  7552  ovig  7579  dfoprab4f  8080  f1o2ndf1  8146  om00el  8613  oeoe  8636  eroveu  8851  endisj  9097  infxpen  10052  dfac5lem4OLD  10166  sornom  10315  ltsrpr  11115  axcnre  11202  axmulgt0  11333  wloglei  11793  mulge0b  12136  addltmul  12500  ltxr  13155  fzadd2  13596  sumsqeq0  14215  ccat0  14611  rlim  15528  cpnnen  16262  dvds2lem  16303  opoe  16397  omoe  16398  opeo  16399  omeo  16400  gcddvds  16537  dfgcd2  16580  pcqmul  16887  xpsfrnel2  17611  eqgval  19208  frgpuplem  19805  mpfind  22149  2ndcctbss  23479  txbasval  23630  cnmpt12  23691  cnmpt22  23698  prdsxmslem2  24558  ishtpy  25018  bcthlem1  25372  bcth  25377  volun  25594  vitali  25662  itg1addlem3  25747  rolle  26043  mumullem2  27238  lgsquadlem3  27441  lgsquad  27442  2sqlem7  27483  scutval  27860  slerec  27879  remulscllem2  28448  axpasch  28971  wlkson  29689  iswwlksnon  29883  wpthswwlks2on  29991  eulplig  30514  hlimi  31217  leopadd  32161  brab2d  32627  eqrelrd2  32636  cntzun  33054  isinftm  33171  finexttrb  33690  metidv  33853  satfv1  35348  satfbrsuc  35351  gonarlem  35379  satfv0fvfmla0  35398  satfv1fvfmla1  35408  altopthg  35949  altopthbg  35950  brsegle  36090  bj-imdirvallem  37163  finxpreclem3  37376  itg2addnclem3  37660  exan3  38276  exanres  38277  exanres3  38278  eqrel2  38281  brcoss  38413  brcoss3  38415  brcoels  38417  br1cossxrnres  38430  brcosscnv  38454  prtlem13  38850  dib1dim  41148  f1o2d2  42253  pellex  42823  tfsconcatb0  43334  tfsconcat00  43337  prsprel  47412  uspgrsprf1  47991  uspgrsprfo  47992