Theorem ifbid 4370

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507  ifcif 4348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2747

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-ex 1743  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-if 4349

This theorem is referenced by:  ifbieq1d  4371  ifbieq2d  4373  ifbieq12d  4375  ifbieq12d2  4381  ifan  4399  ifor  4400  rabsnif  4531  suppsnop  7644  resixpfo  8293  pw2f1olem  8413  unxpdomlem1  8513  cantnflem1d  8941  cantnflem1  8942  dfac12lem1  9359  ttukeylem3  9727  2resupmax  12395  xaddval  12430  xmulcom  12472  xmulneg1  12475  repswswrd  13997  ccatco  14053  sgnval  14302  sumeq1  14900  sumsplit  14977  prodeq1f  15116  rpnnen2lem1  15421  rpnnen2lem2  15422  rpnnen2lem10  15430  sadadd2lem2  15653  sadfval  15655  sadcp1  15658  sadadd2lem  15662  sadcom  15666  pcmpt  16078  pcmpt2  16079  pcfac  16085  prmrec  16108  ramcl  16215  acsfn  16782  setcepi  17200  mgmnsgrpex  17881  sgrpnmndex  17882  frgpup3lem  18657  dpjrid  18928  abvtrivd  19327  psrlidm  19891  psrridm  19892  mvrval  19909  mvrval2  19910  mvrf1  19913  mplmonmul  19952  mplcoe1  19953  mplcoe3  19954  mplcoe5  19956  evlslem3  20001  coe1tm  20138  coe1tmfv2  20140  gsummoncoe1  20169  obsip  20561  uvcval  20625  uvcvval  20626  mat1comp  20747  mamulid  20748  mamurid  20749  mat1ov  20755  mattpos1  20763  mat1dimid  20781  scmateALT  20819  scmatscm  20820  1mavmul  20855  marrepval  20869  marrepeval  20870  marepvval  20874  ma1repveval  20878  1marepvmarrepid  20882  mdetdiagid  20907  mdetunilem8  20926  mdetunilem9  20927  maducoeval  20946  maducoeval2  20947  madutpos  20949  madugsum  20950  minmar1val  20955  minmar1eval  20956  symgmatr01lem  20960  symgmatr01  20961  gsummatr01lem3  20964  gsummatr01lem4  20965  gsummatr01  20966  m2cpm  21047  m2cpminvid2lem  21060  decpmatid  21076  monmatcollpw  21085  mp2pm2mplem4  21115  chmatval  21135  fvmptnn04if  21155  fclsval  22314  tmsxpsval2  22846  dscmet  22879  dscopn  22880  ovolicc1  23814  ovolicc  23821  i1f1lem  23987  itg11  23989  i1fpos  24004  itg2uba  24041  itg2split  24047  itg2monolem1  24048  itg2cnlem1  24059  itg2cnlem2  24060  itg2cn  24061  ibllem  24062  isibl  24063  itgeq1f  24069  itgresr  24076  iblpos  24090  itgposval  24093  i1fibl  24105  ibladdlem  24117  iblabslem  24125  itgcn  24140  coe1termlem  24545  coe1term  24546  cxpval  24942  leibpilem2  25215  leibpi  25216  prmorcht  25451  sqff1o  25455  pclogsum  25487  dchr1  25529  dchr2sum  25545  sum2dchr  25546  lgsval  25573  lgsneg  25593  lgsdilem  25596  lgsdir2  25602  lgsdir  25604  dchrisum0flblem2  25781  dchrisum0flb  25782  ostth1  25905  sgnsv  30459  sgnsval  30460  fzto1st  30685  psgnfzto1st  30687  smatfval  30693  1smat1  30702  indval  30907  indfval  30910  prodindf  30917  ddeval1  31129  ddeval0  31130  eulerpartlemgvv  31270  sgnneg  31435  signsvvfval  31487  signsvfn  31491  hashreprin  31530  circlemeth  31550  kur14  32038  mrsubrn  32250  finxpeq1  34073  poimirlem5  34316  poimirlem6  34317  poimirlem7  34318  poimirlem8  34319  poimirlem10  34321  poimirlem11  34322  poimirlem12  34323  poimirlem15  34326  poimirlem16  34327  poimirlem17  34328  poimirlem18  34329  poimirlem19  34330  poimirlem20  34331  poimirlem21  34332  poimirlem22  34333  poimirlem23  34334  poimirlem27  34338  itg2addnclem  34362  itg2gt0cn  34366  ibladdnclem  34367  iblabsnclem  34374  ftc1anclem5  34390  ftc1anc  34394  ftc2nc  34395  frlmvscadiccat  38560  pw2f1ocnv  39008  flcidc  39148  refsum2cnlem1  40690  icccncfext  41579  fourierdlem112  41913  fourierswlem  41925  fouriersw  41926  etransclem1  41930  etransclem5  41934  etransclem17  41946  etransclem32  41961  etransclem41  41970  hoidmv1lelem2  42284  ovnhoi  42295  hspdifhsp  42308  hspmbl  42321  hoimbl  42323  ovnsubadd2  42338  suppmptcfin  43767  linc0scn0  43819  linc1  43821  lcoss  43832  el0ldep  43862