Theorem ifbid 4512

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

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

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 4489

This theorem is referenced by:  ifbieq1d  4513  ifbieq2d  4515  ifbieq12d  4517  ifbieq12d2  4523  ifan  4542  ifor  4543  rabsnif  4687  suppsnop  8157  resixpfo  8909  pw2f1olem  9045  unxpdomlem1  9197  cantnflem1d  9641  cantnflem1  9642  ssttrcl  9668  ttrclselem2  9679  dfac12lem1  10097  ttukeylem3  10464  2resupmax  13148  xaddval  13183  xmulcom  13226  xmulneg1  13229  repswswrd  14749  ccatco  14801  sgnval  15054  sumeq1  15655  sumsplit  15734  prodeq1f  15872  prodeq1  15873  rpnnen2lem1  16182  rpnnen2lem2  16183  rpnnen2lem10  16191  sadadd2lem2  16420  sadfval  16422  sadcp1  16425  sadadd2lem  16429  sadcom  16433  pcmpt  16863  pcmpt2  16864  pcfac  16870  prmrec  16893  ramcl  17000  acsfn  17620  setcepi  18050  mgmnsgrpex  18858  sgrpnmndex  18859  frgpup3lem  19707  dpjrid  19994  abvtrivd  20741  obsip  21630  uvcval  21694  uvcvval  21695  psrlidm  21871  psrridm  21872  psrascl  21888  mvrval  21891  mvrval2  21892  mvrf1  21895  mplmonmul  21943  mplcoe1  21944  mplcoe3  21945  mplcoe5  21947  evlslem3  21987  mhpsclcl  22034  psdfval  22045  psdmplcl  22049  psdmul  22053  psdmvr  22056  coe1tm  22159  coe1tmfv2  22161  gsummoncoe1  22195  mat1comp  22327  mamulid  22328  mamurid  22329  mat1ov  22335  mattpos1  22343  mat1dimid  22361  scmateALT  22399  scmatscm  22400  1mavmul  22435  marrepval  22449  marrepeval  22450  marepvval  22454  ma1repveval  22458  1marepvmarrepid  22462  mdetdiagid  22487  mdetunilem8  22506  mdetunilem9  22507  maducoeval  22526  maducoeval2  22527  madutpos  22529  madugsum  22530  minmar1val  22535  minmar1eval  22536  symgmatr01lem  22540  symgmatr01  22541  gsummatr01lem3  22544  gsummatr01lem4  22545  gsummatr01  22546  m2cpm  22628  m2cpminvid2lem  22641  decpmatid  22657  monmatcollpw  22666  mp2pm2mplem4  22696  chmatval  22716  fvmptnn04if  22736  fclsval  23895  tmsxpsval2  24427  dscmet  24460  dscopn  24461  ovolicc1  25417  ovolicc  25424  i1f1lem  25590  itg11  25592  i1fpos  25607  itg2uba  25644  itg2split  25650  itg2monolem1  25651  itg2cnlem1  25662  itg2cnlem2  25663  itg2cn  25664  ibllem  25665  isibl  25666  itgeq1f  25672  itgeq1fOLD  25673  itgeq1  25674  cbvitgv  25678  itgresr  25680  iblpos  25694  itgposval  25697  i1fibl  25709  ibladdlem  25721  iblabslem  25729  itgcn  25746  coe1termlem  26163  coe1term  26164  cxpval  26573  leibpilem2  26851  leibpi  26852  prmorcht  27088  sqff1o  27092  pclogsum  27126  dchr1  27168  dchr2sum  27184  sum2dchr  27185  lgsval  27212  lgsneg  27232  lgsdilem  27235  lgsdir2  27241  lgsdir  27243  dchrisum0flblem2  27420  dchrisum0flb  27421  ostth1  27544  mptprop  32621  sgnneg  32758  indval  32776  indfval  32779  prodindf  32786  fzto1st  33060  psgnfzto1st  33062  sgnsv  33117  sgnsval  33118  elrspunsn  33400  smatfval  33785  1smat1  33794  ddeval1  34224  ddeval0  34225  eulerpartlemgvv  34367  signsvvfval  34569  signsvfn  34573  hashreprin  34611  circlemeth  34631  kur14  35203  ex-sategoelel  35408  mrsubrn  35500  prodeq12sdv  36206  itgeq12sdv  36207  cbvitgvw2  36236  cbvitgdavw  36269  cbvitgdavw2  36285  finxpeq1  37374  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem27  37641  itg2addnclem  37665  itg2gt0cn  37669  ibladdnclem  37670  iblabsnclem  37677  ftc1anclem5  37691  ftc1anc  37695  ftc2nc  37696  frlmvscadiccat  42494  fiabv  42524  evlsbagval  42554  selvvvval  42573  fsuppind  42578  pw2f1ocnv  43026  flcidc  43159  cantnfresb  43313  refsum2cnlem1  45031  icccncfext  45885  fourierdlem112  46216  fourierswlem  46228  fouriersw  46229  etransclem1  46233  etransclem5  46237  etransclem17  46249  etransclem32  46264  etransclem41  46273  hoidmv1lelem2  46590  ovnhoi  46601  hspdifhsp  46614  hspmbl  46627  hoimbl  46629  ovnsubadd2  46644  suppmptcfin  48364  linc0scn0  48412  linc1  48414  lcoss  48425  el0ldep  48455