Theorem ifbid 4508

Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)

Hypothesis

Ref	Expression
ifbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
ifbid	⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))

Proof of Theorem ifbid

Step	Hyp	Ref	Expression
1		ifbid.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		ifbi 4507	. 2 ⊢ ((𝜓 ↔ 𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4485

This theorem is referenced by:  ifbieq1d  4509  ifbieq2d  4511  ifbieq12d  4513  ifbieq12d2  4519  ifan  4538  ifor  4539  rabsnif  4683  suppsnop  8134  resixpfo  8886  pw2f1olem  9022  unxpdomlem1  9173  cantnflem1d  9617  cantnflem1  9618  ssttrcl  9644  ttrclselem2  9655  dfac12lem1  10073  ttukeylem3  10440  2resupmax  13124  xaddval  13159  xmulcom  13202  xmulneg1  13205  repswswrd  14725  ccatco  14777  sgnval  15030  sumeq1  15631  sumsplit  15710  prodeq1f  15848  prodeq1  15849  rpnnen2lem1  16158  rpnnen2lem2  16159  rpnnen2lem10  16167  sadadd2lem2  16396  sadfval  16398  sadcp1  16401  sadadd2lem  16405  sadcom  16409  pcmpt  16839  pcmpt2  16840  pcfac  16846  prmrec  16869  ramcl  16976  acsfn  17600  setcepi  18030  mgmnsgrpex  18840  sgrpnmndex  18841  frgpup3lem  19691  dpjrid  19978  abvtrivd  20752  obsip  21663  uvcval  21727  uvcvval  21728  psrlidm  21904  psrridm  21905  psrascl  21921  mvrval  21924  mvrval2  21925  mvrf1  21928  mplmonmul  21976  mplcoe1  21977  mplcoe3  21978  mplcoe5  21980  evlslem3  22020  mhpsclcl  22067  psdfval  22078  psdmplcl  22082  psdmul  22086  psdmvr  22089  coe1tm  22192  coe1tmfv2  22194  gsummoncoe1  22228  mat1comp  22360  mamulid  22361  mamurid  22362  mat1ov  22368  mattpos1  22376  mat1dimid  22394  scmateALT  22432  scmatscm  22433  1mavmul  22468  marrepval  22482  marrepeval  22483  marepvval  22487  ma1repveval  22491  1marepvmarrepid  22495  mdetdiagid  22520  mdetunilem8  22539  mdetunilem9  22540  maducoeval  22559  maducoeval2  22560  madutpos  22562  madugsum  22563  minmar1val  22568  minmar1eval  22569  symgmatr01lem  22573  symgmatr01  22574  gsummatr01lem3  22577  gsummatr01lem4  22578  gsummatr01  22579  m2cpm  22661  m2cpminvid2lem  22674  decpmatid  22690  monmatcollpw  22699  mp2pm2mplem4  22729  chmatval  22749  fvmptnn04if  22769  fclsval  23928  tmsxpsval2  24460  dscmet  24493  dscopn  24494  ovolicc1  25450  ovolicc  25457  i1f1lem  25623  itg11  25625  i1fpos  25640  itg2uba  25677  itg2split  25683  itg2monolem1  25684  itg2cnlem1  25695  itg2cnlem2  25696  itg2cn  25697  ibllem  25698  isibl  25699  itgeq1f  25705  itgeq1fOLD  25706  itgeq1  25707  cbvitgv  25711  itgresr  25713  iblpos  25727  itgposval  25730  i1fibl  25742  ibladdlem  25754  iblabslem  25762  itgcn  25779  coe1termlem  26196  coe1term  26197  cxpval  26606  leibpilem2  26884  leibpi  26885  prmorcht  27121  sqff1o  27125  pclogsum  27159  dchr1  27201  dchr2sum  27217  sum2dchr  27218  lgsval  27245  lgsneg  27265  lgsdilem  27268  lgsdir2  27274  lgsdir  27276  dchrisum0flblem2  27453  dchrisum0flb  27454  ostth1  27577  mptprop  32671  sgnneg  32808  indval  32826  indfval  32829  prodindf  32836  fzto1st  33075  psgnfzto1st  33077  sgnsv  33132  sgnsval  33133  elrspunsn  33393  smatfval  33778  1smat1  33787  ddeval1  34217  ddeval0  34218  eulerpartlemgvv  34360  signsvvfval  34562  signsvfn  34566  hashreprin  34604  circlemeth  34624  kur14  35196  ex-sategoelel  35401  mrsubrn  35493  prodeq12sdv  36199  itgeq12sdv  36200  cbvitgvw2  36229  cbvitgdavw  36262  cbvitgdavw2  36278  finxpeq1  37367  poimirlem5  37612  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem15  37622  poimirlem16  37623  poimirlem17  37624  poimirlem18  37625  poimirlem19  37626  poimirlem20  37627  poimirlem21  37628  poimirlem22  37629  poimirlem23  37630  poimirlem27  37634  itg2addnclem  37658  itg2gt0cn  37662  ibladdnclem  37663  iblabsnclem  37670  ftc1anclem5  37684  ftc1anc  37688  ftc2nc  37689  frlmvscadiccat  42487  fiabv  42517  evlsbagval  42547  selvvvval  42566  fsuppind  42571  pw2f1ocnv  43019  flcidc  43152  cantnfresb  43306  refsum2cnlem1  45024  icccncfext  45878  fourierdlem112  46209  fourierswlem  46221  fouriersw  46222  etransclem1  46226  etransclem5  46230  etransclem17  46242  etransclem32  46257  etransclem41  46266  hoidmv1lelem2  46583  ovnhoi  46594  hspdifhsp  46607  hspmbl  46620  hoimbl  46622  ovnsubadd2  46637  suppmptcfin  48357  linc0scn0  48405  linc1  48407  lcoss  48418  el0ldep  48448