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 594	1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  bi2anan9r  636  rspc2gv  3620  2reu5  3753  ralprgf  4695  ralprg  4697  raltpg  4701  prssg  4821  prsspwg  4825  ssprss  4826  intprg  4984  opelopab2a  5534  opelxp  5711  eqrel  5783  eqrelrel  5796  brcog  5865  tpres  7203  dff13  7256  resoprab2  7529  ovig  7556  dfoprab4f  8044  f1o2ndf1  8110  om00el  8578  oeoe  8601  eroveu  8808  endisj  9060  infxpen  10011  dfac5lem4  10123  sornom  10274  ltsrpr  11074  axcnre  11161  axmulgt0  11292  wloglei  11750  mulge0b  12088  addltmul  12452  ltxr  13099  fzadd2  13540  sumsqeq0  14147  ccat0  14530  rlim  15443  cpnnen  16176  dvds2lem  16216  opoe  16310  omoe  16311  opeo  16312  omeo  16313  gcddvds  16448  dfgcd2  16492  pcqmul  16790  xpsfrnel2  17514  eqgval  19093  frgpuplem  19681  mpfind  21889  2ndcctbss  23179  txbasval  23330  cnmpt12  23391  cnmpt22  23398  prdsxmslem2  24258  ishtpy  24718  bcthlem1  25072  bcth  25077  volun  25294  vitali  25362  itg1addlem3  25447  rolle  25742  mumullem2  26920  lgsquadlem3  27121  lgsquad  27122  2sqlem7  27163  scutval  27538  slerec  27557  axpasch  28466  wlkson  29180  iswwlksnon  29374  wpthswwlks2on  29482  eulplig  30005  hlimi  30708  leopadd  31652  eqrelrd2  32112  cntzun  32482  isinftm  32597  finexttrb  33029  metidv  33170  satfv1  34652  satfbrsuc  34655  gonarlem  34683  satfv0fvfmla0  34702  satfv1fvfmla1  34712  altopthg  35243  altopthbg  35244  brsegle  35384  bj-imdirvallem  36364  finxpreclem3  36577  itg2addnclem3  36844  exan3  37466  exanres  37467  exanres3  37468  eqrel2  37471  brcoss  37604  brcoss3  37606  brcoels  37608  br1cossxrnres  37621  brcosscnv  37645  prtlem13  38041  dib1dim  40339  f1o2d2  41361  pellex  41875  tfsconcatb0  42396  tfsconcat00  42399  prsprel  46453  uspgrsprf1  46823  uspgrsprfo  46824