Theorem bi2anan9 649

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  bi2anan9r  650  rspc2gv  3600  2reu5  3730  ralprgf  4665  ralprg  4667  raltpg  4669  prssg  4789  prsspwg  4793  ssprss  4794  intprg  4950  opelopab2a  5520  brab2d  5523  opelxp  5698  eqrel  5771  eqrelrel  5784  brcog  5853  tpres  7200  dff13  7253  cbvmpov  7506  resoprab2  7530  ovig  7557  dfoprab4f  8053  f1o2ndf1  8117  mpof1o2d  8121  om00el  8561  oeoe  8585  eroveu  8810  endisj  9052  infxpen  9998  sornom  10261  ltsrpr  11062  axcnre  11149  axmulgt0  11284  wloglei  11746  mulge0b  12085  addltmul  12480  ltxr  13140  fzadd2  13587  sumsqeq0  14215  ccat0  14613  rlim  15546  cpnnen  16285  dvds2lem  16326  opoe  16421  omoe  16422  opeo  16423  omeo  16424  gcddvds  16561  dfgcd2  16604  pcqmul  16913  xpsfrnel2  17618  eqgval  19245  frgpuplem  19842  mpfind  22235  2ndcctbss  23581  txbasval  23732  cnmpt12  23793  cnmpt22  23800  prdsxmslem2  24655  ishtpy  25100  bcthlem1  25452  bcth  25457  volun  25673  vitali  25741  itg1addlem3  25826  rolle  26118  mumullem2  27310  lgsquadlem3  27512  lgsquad  27513  2sqlem7  27554  cutsval  27939  lesrec  27958  remulscllem2  28660  elplngid  29022  lnincplng  29024  plngcp  29026  plngrot  29030  nhpmirhp  29038  lnperpexs  29071  ragraghl  29104  brprlng  29143  prlnghpg  29151  prlngmo  29157  axpasch  29232  wlkson  29945  iswwlksnon  30143  wpthswwlks2on  30254  eulplig  30778  hlimi  31481  leopadd  32425  tpssg  32824  eqrelrd2  32902  cntzun  33340  isinftm  33442  finexttrb  34000  metidv  34227  satfv1  35788  satfbrsuc  35791  gonarlem  35819  satfv0fvfmla0  35838  satfv1fvfmla1  35848  altopthg  36392  altopthbg  36393  brsegle  36533  bj-imdirvallem  37746  finxpreclem3  37961  itg2addnclem3  38246  exan3  38873  exanres  38874  exanres3  38875  eqrel2  38878  sucmapleftuniq  39063  brcoss  39094  brcoss3  39096  brcoels  39098  br1cossxrnres  39111  brcosscnv  39135  disjimeceqim2  39378  eldisjim3  39388  prtlem13  39566  dib1dim  41863  pellex  43488  tfsconcatb0  43997  tfsconcat00  44000  prsprel  48159  uspgrsprf1  48835  uspgrsprfo  48836  brab2ddw2  49527