Theorem ifbid 4108

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  ifbieq1d  4109  ifbieq2d  4111  ifbieq12d  4113  ifbieq12d2  4119  ifan  4134  ifor  4135  rabsnif  4258  suppsnop  7309  resixpfo  7946  pw2f1olem  8064  unxpdomlem1  8164  cantnflem1d  8585  cantnflem1  8586  dfac12lem1  8965  ttukeylem3  9333  2resupmax  12019  xaddval  12054  xmulcom  12096  xmulneg1  12099  repswswrd  13531  ccatco  13581  sgnval  13828  sumeq1  14419  sumsplit  14499  prodeq1f  14638  rpnnen2lem1  14943  rpnnen2lem2  14944  rpnnen2lem10  14952  sadadd2lem2  15172  sadfval  15174  sadcp1  15177  sadadd2lem  15181  sadcom  15185  pcmpt  15596  pcmpt2  15597  pcfac  15603  prmrec  15626  ramcl  15733  acsfn  16320  setcepi  16738  mgmnsgrpex  17418  sgrpnmndex  17419  frgpup3lem  18190  dpjrid  18461  abvtrivd  18840  psrlidm  19403  psrridm  19404  mvrval  19421  mvrval2  19422  mvrf1  19425  mplmonmul  19464  mplcoe1  19465  mplcoe3  19466  mplcoe5  19468  evlslem3  19514  coe1tm  19643  coe1tmfv2  19645  gsummoncoe1  19674  obsip  20065  uvcval  20124  uvcvval  20125  mat1comp  20246  mamulid  20247  mamurid  20248  mat1ov  20254  mattpos1  20262  mat1dimid  20280  scmateALT  20318  scmatscm  20319  1mavmul  20354  marrepval  20368  marrepeval  20369  marepvval  20373  ma1repveval  20377  1marepvmarrepid  20381  mdetdiagid  20406  mdetunilem8  20425  mdetunilem9  20426  maducoeval  20445  maducoeval2  20446  madutpos  20448  madugsum  20449  minmar1val  20454  minmar1eval  20455  symgmatr01lem  20459  symgmatr01  20460  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  m2cpm  20546  m2cpminvid2lem  20559  decpmatid  20575  monmatcollpw  20584  mp2pm2mplem4  20614  chmatval  20634  fvmptnn04if  20654  fclsval  21812  tmsxpsval2  22344  dscmet  22377  dscopn  22378  ovolicc1  23284  ovolicc  23291  i1f1lem  23456  itg11  23458  i1fpos  23473  itg2uba  23510  itg2split  23516  itg2monolem1  23517  itg2cnlem1  23528  itg2cnlem2  23529  itg2cn  23530  ibllem  23531  isibl  23532  itgeq1f  23538  itgresr  23545  iblpos  23559  itgposval  23562  i1fibl  23574  ibladdlem  23586  iblabslem  23594  itgcn  23609  coe1termlem  24014  coe1term  24015  cxpval  24410  leibpilem2  24668  leibpi  24669  prmorcht  24904  sqff1o  24908  pclogsum  24940  dchr1  24982  dchr2sum  24998  sum2dchr  24999  lgsval  25026  lgsneg  25046  lgsdilem  25049  lgsdir2  25055  lgsdir  25057  dchrisum0flblem2  25198  dchrisum0flb  25199  ostth1  25322  sgnsv  29727  sgnsval  29728  fzto1st  29853  psgnfzto1st  29855  smatfval  29861  1smat1  29870  indval  30075  indfval  30078  prodindf  30085  ddeval1  30297  ddeval0  30298  eulerpartlemgvv  30438  sgnneg  30602  signsvvfval  30655  signsvfn  30659  hashreprin  30698  circlemeth  30718  kur14  31198  mrsubrn  31410  finxpeq1  33223  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem27  33436  itg2addnclem  33461  itg2gt0cn  33465  ibladdnclem  33466  iblabsnclem  33473  ftc1anclem5  33489  ftc1anc  33493  ftc2nc  33494  pw2f1ocnv  37604  flcidc  37744  refsum2cnlem1  39196  icccncfext  40100  fourierdlem112  40435  fourierswlem  40447  fouriersw  40448  etransclem1  40452  etransclem5  40456  etransclem17  40468  etransclem32  40483  etransclem41  40492  hoidmv1lelem2  40806  ovnhoi  40817  hspdifhsp  40830  hspmbl  40843  hoimbl  40845  ovnsubadd2  40860  suppmptcfin  42160  linc0scn0  42212  linc1  42214  lcoss  42225  el0ldep  42255