Theorem ifbid 4505

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 4504	. 2 ⊢ ((𝜓 ↔ 𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1561  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4482

This theorem is referenced by:  ifbieq1d  4506  ifbieq2d  4508  ifbieq12d  4510  ifbieq12d2  4516  ifan  4535  ifor  4536  rabsnif  4683  suppsnop  8159  resixpfo  8919  pw2f1olem  9054  unxpdomlem1  9201  cantnflem1d  9644  cantnflem1  9645  ssttrcl  9671  ttrclselem2  9682  dfac12lem1  10101  ttukeylem3  10469  indval  12199  indfval  12203  2resupmax  13192  xaddval  13227  xmulcom  13270  xmulneg1  13273  repswswrd  14798  ccatco  14849  sgnval  15102  sgnneg  15114  sumeq1  15717  sumsplit  15796  prodeq1f  15937  prodeq1  15938  rpnnen2lem1  16247  rpnnen2lem2  16248  rpnnen2lem10  16256  sadadd2lem2  16485  sadfval  16487  sadcp1  16490  sadadd2lem  16494  sadcom  16498  pcmpt  16929  pcmpt2  16930  pcfac  16936  prmrec  16959  ramcl  17066  acsfn  17692  setcepi  18122  mgmnsgrpex  18969  sgrpnmndex  18970  frgpup3lem  19818  dpjrid  20105  abvtrivd  20882  obsip  21774  uvcval  21838  uvcvval  21839  psrlidm  22014  psrridm  22015  psrascl  22031  mvrval  22034  mvrval2  22035  mvrf1  22038  mplmonmul  22090  mplcoe1  22091  mplcoe3  22092  mplcoe5  22094  evlslem3  22134  selvvvval  22196  mhpsclcl  22213  psdfval  22224  psdmplcl  22228  psdmul  22232  psdmvr  22235  coe1tm  22337  coe1tmfv2  22339  gsummoncoe1  22372  mat1comp  22501  mamulid  22502  mamurid  22503  mat1ov  22509  mattpos1  22517  mat1dimid  22535  scmateALT  22573  scmatscm  22574  1mavmul  22609  marrepval  22623  marrepeval  22624  marepvval  22628  ma1repveval  22632  1marepvmarrepid  22636  mdetdiagid  22661  mdetunilem8  22680  mdetunilem9  22681  maducoeval  22700  maducoeval2  22701  madutpos  22703  madugsum  22704  minmar1val  22709  minmar1eval  22710  symgmatr01lem  22714  symgmatr01  22715  gsummatr01lem3  22718  gsummatr01lem4  22719  gsummatr01  22720  m2cpm  22802  m2cpminvid2lem  22815  decpmatid  22831  monmatcollpw  22840  mp2pm2mplem4  22870  chmatval  22890  fvmptnn04if  22910  fclsval  24069  tmsxpsval2  24600  dscmet  24633  dscopn  24634  ovolicc1  25579  ovolicc  25586  i1f1lem  25752  itg11  25754  i1fpos  25769  itg2uba  25806  itg2split  25812  itg2monolem1  25813  itg2cnlem1  25824  itg2cnlem2  25825  itg2cn  25826  ibllem  25827  isibl  25828  itgeq1f  25834  itgeq1fOLD  25835  itgeq1  25836  cbvitgv  25840  itgresr  25842  iblpos  25856  itgposval  25859  i1fibl  25871  ibladdlem  25883  iblabslem  25891  itgcn  25908  coe1termlem  26319  coe1term  26320  cxpval  26730  leibpilem2  27007  leibpi  27008  prmorcht  27243  sqff1o  27247  pclogsum  27280  dchr1  27322  dchr2sum  27338  sum2dchr  27339  lgsval  27366  lgsneg  27386  lgsdilem  27389  lgsdir2  27395  lgsdir  27397  dchrisum0flblem2  27574  dchrisum0flb  27575  ostth1  27698  partfun2  32879  mptprop  32901  prodindf  33041  indsn  33042  fzto1st  33284  psgnfzto1st  33286  sgnsv  33341  sgnsval  33342  elrspunsn  33616  mvrvalind  33836  mplvrpmrhm  33845  psrmonmul  33848  psrmonmul2  33849  psrmonprod  33850  mplmonprod  33852  esplysply  33869  esplyfval1  33871  esplyfvaln  33872  esplyind  33873  smatfval  34093  1smat1  34102  ddeval1  34532  ddeval0  34533  eulerpartlemgvv  34674  signsvvfval  34873  signsvfn  34877  hashreprin  34915  circlemeth  34935  kur14  35567  ex-sategoelel  35772  mrsubrn  35864  prodeq12sdv  36579  itgeq12sdv  36580  cbvitgvw2  36609  cbvitgdavw  36642  cbvitgdavw2  36658  finxpeq1  37881  poimirlem5  38125  poimirlem6  38126  poimirlem7  38127  poimirlem8  38128  poimirlem10  38130  poimirlem11  38131  poimirlem12  38132  poimirlem15  38135  poimirlem16  38136  poimirlem17  38137  poimirlem18  38138  poimirlem19  38139  poimirlem20  38140  poimirlem21  38141  poimirlem22  38142  poimirlem23  38143  poimirlem27  38147  itg2addnclem  38171  itg2gt0cn  38175  ibladdnclem  38176  iblabsnclem  38183  ftc1anclem5  38197  ftc1anc  38201  ftc2nc  38202  frlmvscadiccat  43129  fiabv  43155  evlsbagval  43169  fsuppind  43173  pw2f1ocnv  43615  flcidc  43748  cantnfresb  43902  refsum2cnlem1  45618  icccncfext  46462  fourierdlem112  46793  fourierswlem  46805  fouriersw  46806  etransclem1  46810  etransclem5  46814  etransclem17  46826  etransclem32  46841  etransclem41  46850  hoidmv1lelem2  47167  ovnhoi  47178  hspdifhsp  47191  hspmbl  47204  hoimbl  47206  ovnsubadd2  47221  suppmptcfin  48999  linc0scn0  49046  linc1  49048  lcoss  49059  el0ldep  49089