Theorem bi2anan9 650

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bi2anan9r  651  rspc2gv  3589  2reu5  3719  ralprgf  4658  ralprg  4660  raltpg  4662  prssg  4783  prsspwg  4787  ssprss  4788  intprg  4944  opelopab2a  5517  brab2d  5520  opelxp  5695  eqrel  5768  eqrelrel  5781  brcog  5850  tpres  7204  dff13  7255  cbvmpov  7512  resoprab2  7536  ovig  7563  dfoprab4f  8057  f1o2ndf1  8123  mpof1o2d  8127  om00el  8567  oeoe  8591  eroveu  8816  endisj  9066  infxpen  10021  sornom  10283  ltsrpr  11090  axcnre  11177  axmulgt0  11312  wloglei  11774  mulge0b  12113  addltmul  12508  ltxr  13170  fzadd2  13618  sumsqeq0  14247  ccat0  14645  rlim  15586  cpnnen  16323  dvds2lem  16364  opoe  16459  omoe  16460  opeo  16461  omeo  16462  gcddvds  16599  dfgcd2  16642  pcqmul  16951  xpsfrnel2  17656  eqgval  19308  frgpuplem  19905  mpfind  22337  2ndcctbss  23687  txbasval  23838  cnmpt12  23899  cnmpt22  23906  prdsxmslem2  24761  ishtpy  25206  bcthlem1  25558  bcth  25563  volun  25779  vitali  25847  itg1addlem3  25932  rolle  26224  mumullem2  27424  lgsquadlem3  27626  lgsquad  27627  2sqlem7  27668  cutsval  28053  lesrec  28072  remulscllem2  28774  elplngid  29147  lnincplng  29149  plngcp  29151  plngrot  29155  nhpmirhp  29163  lnperpexs  29197  ragraghl  29233  tgaaddcpbllem2  29237  brprlng  29303  prlnghpg  29311  prlngmo  29319  axpasch  29406  wlkson  30122  iswwlksnon  30329  wpthswwlks2on  30440  eulplig  30974  hlimi  31677  leopadd  32621  tpssg  33020  eqrelrd2  33097  cntzun  33527  isinftm  33629  finexttrb  34183  metidv  34410  satfv1  35950  satfbrsuc  35953  gonarlem  35981  satfv0fvfmla0  36000  satfv1fvfmla1  36010  altopthg  36555  altopthbg  36556  brsegle  36696  nmuladdss  36801  bj-imdirvallem  37940  finxpreclem3  38155  itg2addnclem3  38430  exan3  39056  exanres  39057  exanres3  39058  eqrel2  39061  sucmapleftuniq  39246  brcoss  39277  brcoss3  39279  brcoels  39281  br1cossxrnres  39294  brcosscnv  39318  disjimeceqim2  39561  eldisjim3  39571  prtlem13  39749  dib1dim  42046  pellex  43684  tfsconcatb0  44193  tfsconcat00  44196  prsprel  48395  uspgrsprf1  49071  uspgrsprfo  49072  brab2ddw2  49766