Theorem ifbid 4506

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4483

This theorem is used by:  ifbieq1d  4507  ifbieq2d  4509  ifbieq12d  4511  ifbieq12d2  4517  ifan  4536  ifor  4537  rabsnif  4684  suppsnop  8177  resixpfo  8946  pw2f1olem  9082  unxpdomlem1  9229  cantnflem1d  9670  cantnflem1  9671  ssttrcl  9697  ttrclselem2  9708  dfac12lem1  10149  ttukeylem3  10516  indval  12248  indfval  12252  2resupmax  13243  xaddval  13278  xmulcom  13321  xmulneg1  13324  repswswrd  14858  ccatco  14909  sgnval  15164  sgnneg  15176  sumeq1  15779  sumsplit  15857  prodeq1f  15998  prodeq1  15999  rpnnen2lem1  16305  rpnnen2lem2  16306  rpnnen2lem10  16314  sadadd2lem2  16543  sadfval  16545  sadcp1  16548  sadadd2lem  16552  sadcom  16556  pcmpt  16987  pcmpt2  16988  pcfac  16994  prmrec  17017  ramcl  17124  acsfn  17750  setcepi  18180  mgmnsgrpex  19046  sgrpnmndex  19047  frgpup3lem  19907  dpjrid  20194  abvtrivd  21001  obsip  21937  uvcval  22001  uvcvval  22002  psrlidm  22179  psrridm  22180  psrascl  22196  mvrval  22199  mvrval2  22200  mvrf1  22203  mplmonmul  22255  mplcoe1  22256  mplcoe3  22257  mplcoe5  22259  evlslem3  22299  selvvvval  22361  mhpsclcl  22378  psdfval  22389  psdmplcl  22393  psdmul  22397  psdmvr  22400  coe1tm  22502  coe1tmfv2  22504  gsummoncoe1  22536  mat1comp  22665  mamulid  22666  mamurid  22667  mat1ov  22673  mattpos1  22681  mat1dimid  22699  scmateALT  22737  scmatscm  22738  1mavmul  22773  marrepval  22787  marrepeval  22788  marepvval  22792  ma1repveval  22796  1marepvmarrepid  22800  mdetdiagid  22825  mdetunilem8  22844  mdetunilem9  22845  maducoeval  22864  maducoeval2  22865  madutpos  22867  madugsum  22868  minmar1val  22873  minmar1eval  22874  symgmatr01lem  22878  symgmatr01  22879  gsummatr01lem3  22882  gsummatr01lem4  22883  gsummatr01  22884  m2cpm  22969  m2cpminvid2lem  22982  decpmatid  22998  monmatcollpw  23007  mp2pm2mplem4  23037  chmatval  23057  fvmptnn04if  23077  fclsval  24237  tmsxpsval2  24768  dscmet  24801  dscopn  24802  ovolicc1  25747  ovolicc  25754  i1f1lem  25920  itg11  25922  i1fpos  25937  itg2uba  25974  itg2split  25980  itg2monolem1  25981  itg2cnlem1  25992  itg2cnlem2  25993  itg2cn  25994  ibllem  25995  isibl  25996  itgeq1f  26002  itgeq1  26003  cbvitgv  26007  itgresr  26009  iblpos  26023  itgposval  26026  i1fibl  26038  ibladdlem  26050  iblabslem  26058  itgcn  26075  coe1termlem  26487  coe1term  26488  cxpval  26904  leibpilem2  27181  leibpi  27182  prmorcht  27417  sqff1o  27421  pclogsum  27454  dchr1  27496  dchr2sum  27512  sum2dchr  27513  lgsval  27540  lgsneg  27560  lgsdilem  27563  lgsdir2  27569  lgsdir  27571  dchrisum0flblem2  27748  dchrisum0flb  27749  ostth1  27872  partfun2  33152  mptprop  33173  prodindf  33311  indsn  33312  fzto1st  33546  psgnfzto1st  33548  sgnsv  33603  sgnsval  33604  elrspunsn  33860  mvrvalind  34051  mplvrpmrhm  34060  psrmonmul  34063  psrmonmul2  34064  psrmonprod  34065  mplmonprod  34067  esplysply  34084  esplyfval1  34086  esplyfvaln  34087  esplyind  34088  smatfval  34308  1smat1  34317  ddeval1  34748  ddeval0  34749  eulerpartlemgvv  34890  signsvvfval  35089  signsvfn  35093  hashreprin  35131  circlemeth  35151  kur14  35798  ex-sategoelel  36003  mrsubrn  36095  prodeq12sdv  36841  itgeq12sdv  36842  cbvitgvw2  36871  cbvitgdavw  36904  cbvitgdavw2  36920  finxpeq1  38143  poimirlem5  38377  poimirlem6  38378  poimirlem7  38379  poimirlem8  38380  poimirlem10  38382  poimirlem11  38383  poimirlem12  38384  poimirlem15  38387  poimirlem16  38388  poimirlem17  38389  poimirlem18  38390  poimirlem19  38391  poimirlem20  38392  poimirlem21  38393  poimirlem22  38394  poimirlem23  38395  poimirlem27  38399  itg2addnclem  38423  itg2gt0cn  38427  ibladdnclem  38428  iblabsnclem  38435  ftc1anclem5  38449  ftc1anc  38453  ftc2nc  38454  frlmvscadiccat  43397  fiabv  43421  evlsbagval  43435  fsuppind  43439  pw2f1ocnv  43881  flcidc  44014  cantnfresb  44168  refsum2cnlem1  45874  icccncfext  46718  fourierdlem112  47049  fourierswlem  47061  fouriersw  47062  etransclem1  47066  etransclem5  47070  etransclem17  47082  etransclem32  47097  etransclem41  47106  hoidmv1lelem2  47423  ovnhoi  47434  hspdifhsp  47447  hspmbl  47460  hoimbl  47462  ovnsubadd2  47477  suppmptcfin  49309  linc0scn0  49356  linc1  49358  lcoss  49369  el0ldep  49399