Theorem bi2anan9 647

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  bi2anan9r  648  rspc2gv  3593  2reu5  3723  ralprgf  4655  ralprg  4657  raltpg  4659  prssg  4779  prsspwg  4783  ssprss  4784  intprg  4941  opelopab2a  5507  brab2d  5510  opelxp  5685  eqrel  5758  eqrelrel  5771  brcog  5840  tpres  7187  dff13  7240  cbvmpov  7493  resoprab2  7517  ovig  7544  dfoprab4f  8039  f1o2ndf1  8103  mpof1o2d  8107  om00el  8547  oeoe  8571  eroveu  8796  endisj  9038  infxpen  9972  dfac5lem4OLD  10086  sornom  10236  ltsrpr  11037  axcnre  11124  axmulgt0  11259  wloglei  11721  mulge0b  12064  addltmul  12459  ltxr  13119  fzadd2  13566  sumsqeq0  14194  ccat0  14591  rlim  15524  cpnnen  16263  dvds2lem  16304  opoe  16399  omoe  16400  opeo  16401  omeo  16402  gcddvds  16539  dfgcd2  16582  pcqmul  16891  xpsfrnel2  17596  eqgval  19220  frgpuplem  19814  mpfind  22170  2ndcctbss  23517  txbasval  23668  cnmpt12  23729  cnmpt22  23736  prdsxmslem2  24591  ishtpy  25036  bcthlem1  25388  bcth  25393  volun  25609  vitali  25677  itg1addlem3  25762  rolle  26054  mumullem2  27246  lgsquadlem3  27448  lgsquad  27449  2sqlem7  27490  cutsval  27875  lesrec  27894  remulscllem2  28596  elplngid  28991  lnincplng  28993  plngcp  28995  plngrot  28999  brprlng  29067  axpasch  29144  wlkson  29857  iswwlksnon  30055  wpthswwlks2on  30166  eulplig  30690  hlimi  31393  leopadd  32337  tpssg  32738  eqrelrd2  32820  cntzun  33261  isinftm  33363  finexttrb  33964  metidv  34191  satfv1  35718  satfbrsuc  35721  gonarlem  35749  satfv0fvfmla0  35768  satfv1fvfmla1  35778  altopthg  36322  altopthbg  36323  brsegle  36463  bj-imdirvallem  37677  finxpreclem3  37892  itg2addnclem3  38177  exan3  38804  exanres  38805  exanres3  38806  eqrel2  38809  sucmapleftuniq  38994  brcoss  39025  brcoss3  39027  brcoels  39029  br1cossxrnres  39042  brcosscnv  39066  disjimeceqim2  39309  eldisjim3  39319  prtlem13  39497  dib1dim  41794  pellex  43417  tfsconcatb0  43926  tfsconcat00  43929  prsprel  48098  uspgrsprf1  48774  uspgrsprfo  48775  brab2ddw2  49456