Theorem ifbid 4490

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  ifbieq1d  4491  ifbieq2d  4493  ifbieq12d  4495  ifbieq12d2  4501  ifan  4520  ifor  4521  rabsnif  4667  suppsnop  8128  resixpfo  8884  pw2f1olem  9019  unxpdomlem1  9166  cantnflem1d  9609  cantnflem1  9610  ssttrcl  9636  ttrclselem2  9647  dfac12lem1  10066  ttukeylem3  10433  indval  12162  indfval  12166  2resupmax  13140  xaddval  13175  xmulcom  13218  xmulneg1  13221  repswswrd  14746  ccatco  14797  sgnval  15050  sumeq1  15651  sumsplit  15730  prodeq1f  15871  prodeq1  15872  rpnnen2lem1  16181  rpnnen2lem2  16182  rpnnen2lem10  16190  sadadd2lem2  16419  sadfval  16421  sadcp1  16424  sadadd2lem  16428  sadcom  16432  pcmpt  16863  pcmpt2  16864  pcfac  16870  prmrec  16893  ramcl  17000  acsfn  17625  setcepi  18055  mgmnsgrpex  18902  sgrpnmndex  18903  frgpup3lem  19752  dpjrid  20039  abvtrivd  20809  obsip  21701  uvcval  21765  uvcvval  21766  psrlidm  21940  psrridm  21941  psrascl  21957  mvrval  21960  mvrval2  21961  mvrf1  21964  mplmonmul  22014  mplcoe1  22015  mplcoe3  22016  mplcoe5  22018  evlslem3  22058  mhpsclcl  22113  psdfval  22124  psdmplcl  22128  psdmul  22132  psdmvr  22135  coe1tm  22238  coe1tmfv2  22240  gsummoncoe1  22273  mat1comp  22405  mamulid  22406  mamurid  22407  mat1ov  22413  mattpos1  22421  mat1dimid  22439  scmateALT  22477  scmatscm  22478  1mavmul  22513  marrepval  22527  marrepeval  22528  marepvval  22532  ma1repveval  22536  1marepvmarrepid  22540  mdetdiagid  22565  mdetunilem8  22584  mdetunilem9  22585  maducoeval  22604  maducoeval2  22605  madutpos  22607  madugsum  22608  minmar1val  22613  minmar1eval  22614  symgmatr01lem  22618  symgmatr01  22619  gsummatr01lem3  22622  gsummatr01lem4  22623  gsummatr01  22624  m2cpm  22706  m2cpminvid2lem  22719  decpmatid  22735  monmatcollpw  22744  mp2pm2mplem4  22774  chmatval  22794  fvmptnn04if  22814  fclsval  23973  tmsxpsval2  24504  dscmet  24537  dscopn  24538  ovolicc1  25483  ovolicc  25490  i1f1lem  25656  itg11  25658  i1fpos  25673  itg2uba  25710  itg2split  25716  itg2monolem1  25717  itg2cnlem1  25728  itg2cnlem2  25729  itg2cn  25730  ibllem  25731  isibl  25732  itgeq1f  25738  itgeq1fOLD  25739  itgeq1  25740  cbvitgv  25744  itgresr  25746  iblpos  25760  itgposval  25763  i1fibl  25775  ibladdlem  25787  iblabslem  25795  itgcn  25812  coe1termlem  26223  coe1term  26224  cxpval  26628  leibpilem2  26905  leibpi  26906  prmorcht  27141  sqff1o  27145  pclogsum  27178  dchr1  27220  dchr2sum  27236  sum2dchr  27237  lgsval  27264  lgsneg  27284  lgsdilem  27287  lgsdir2  27293  lgsdir  27295  dchrisum0flblem2  27472  dchrisum0flb  27473  ostth1  27596  partfun2  32749  mptprop  32771  sgnneg  32906  prodindf  32922  indsn  32923  fzto1st  33164  psgnfzto1st  33166  sgnsv  33221  sgnsval  33222  elrspunsn  33489  mvrvalind  33682  mplvrpmrhm  33691  psrmonmul  33694  psrmonmul2  33695  psrmonprod  33696  mplmonprod  33698  esplysply  33715  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  smatfval  33939  1smat1  33948  ddeval1  34378  ddeval0  34379  eulerpartlemgvv  34520  signsvvfval  34722  signsvfn  34726  hashreprin  34764  circlemeth  34784  kur14  35398  ex-sategoelel  35603  mrsubrn  35695  prodeq12sdv  36400  itgeq12sdv  36401  cbvitgvw2  36430  cbvitgdavw  36463  cbvitgdavw2  36479  finxpeq1  37702  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem27  37968  itg2addnclem  37992  itg2gt0cn  37996  ibladdnclem  37997  iblabsnclem  38004  ftc1anclem5  38018  ftc1anc  38022  ftc2nc  38023  frlmvscadiccat  42951  fiabv  42981  evlsbagval  43002  selvvvval  43018  fsuppind  43023  pw2f1ocnv  43465  flcidc  43598  cantnfresb  43752  refsum2cnlem1  45468  icccncfext  46315  fourierdlem112  46646  fourierswlem  46658  fouriersw  46659  etransclem1  46663  etransclem5  46667  etransclem17  46679  etransclem32  46694  etransclem41  46703  hoidmv1lelem2  47020  ovnhoi  47031  hspdifhsp  47044  hspmbl  47057  hoimbl  47059  ovnsubadd2  47074  suppmptcfin  48852  linc0scn0  48899  linc1  48901  lcoss  48912  el0ldep  48942