Theorem ifbid 4491

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  ifbieq1d  4492  ifbieq2d  4494  ifbieq12d  4496  ifbieq12d2  4502  ifan  4521  ifor  4522  rabsnif  4668  suppsnop  8122  resixpfo  8878  pw2f1olem  9013  unxpdomlem1  9160  cantnflem1d  9603  cantnflem1  9604  ssttrcl  9630  ttrclselem2  9641  dfac12lem1  10060  ttukeylem3  10427  indval  12156  indfval  12160  2resupmax  13134  xaddval  13169  xmulcom  13212  xmulneg1  13215  repswswrd  14740  ccatco  14791  sgnval  15044  sumeq1  15645  sumsplit  15724  prodeq1f  15865  prodeq1  15866  rpnnen2lem1  16175  rpnnen2lem2  16176  rpnnen2lem10  16184  sadadd2lem2  16413  sadfval  16415  sadcp1  16418  sadadd2lem  16422  sadcom  16426  pcmpt  16857  pcmpt2  16858  pcfac  16864  prmrec  16887  ramcl  16994  acsfn  17619  setcepi  18049  mgmnsgrpex  18896  sgrpnmndex  18897  frgpup3lem  19746  dpjrid  20033  abvtrivd  20803  obsip  21714  uvcval  21778  uvcvval  21779  psrlidm  21953  psrridm  21954  psrascl  21970  mvrval  21973  mvrval2  21974  mvrf1  21977  mplmonmul  22027  mplcoe1  22028  mplcoe3  22029  mplcoe5  22031  evlslem3  22071  mhpsclcl  22126  psdfval  22137  psdmplcl  22141  psdmul  22145  psdmvr  22148  coe1tm  22251  coe1tmfv2  22253  gsummoncoe1  22286  mat1comp  22418  mamulid  22419  mamurid  22420  mat1ov  22426  mattpos1  22434  mat1dimid  22452  scmateALT  22490  scmatscm  22491  1mavmul  22526  marrepval  22540  marrepeval  22541  marepvval  22545  ma1repveval  22549  1marepvmarrepid  22553  mdetdiagid  22578  mdetunilem8  22597  mdetunilem9  22598  maducoeval  22617  maducoeval2  22618  madutpos  22620  madugsum  22621  minmar1val  22626  minmar1eval  22627  symgmatr01lem  22631  symgmatr01  22632  gsummatr01lem3  22635  gsummatr01lem4  22636  gsummatr01  22637  m2cpm  22719  m2cpminvid2lem  22732  decpmatid  22748  monmatcollpw  22757  mp2pm2mplem4  22787  chmatval  22807  fvmptnn04if  22827  fclsval  23986  tmsxpsval2  24517  dscmet  24550  dscopn  24551  ovolicc1  25496  ovolicc  25503  i1f1lem  25669  itg11  25671  i1fpos  25686  itg2uba  25723  itg2split  25729  itg2monolem1  25730  itg2cnlem1  25741  itg2cnlem2  25742  itg2cn  25743  ibllem  25744  isibl  25745  itgeq1f  25751  itgeq1fOLD  25752  itgeq1  25753  cbvitgv  25757  itgresr  25759  iblpos  25773  itgposval  25776  i1fibl  25788  ibladdlem  25800  iblabslem  25808  itgcn  25825  coe1termlem  26236  coe1term  26237  cxpval  26644  leibpilem2  26921  leibpi  26922  prmorcht  27158  sqff1o  27162  pclogsum  27195  dchr1  27237  dchr2sum  27253  sum2dchr  27254  lgsval  27281  lgsneg  27301  lgsdilem  27304  lgsdir2  27310  lgsdir  27312  dchrisum0flblem2  27489  dchrisum0flb  27490  ostth1  27613  partfun2  32767  mptprop  32789  sgnneg  32924  prodindf  32940  indsn  32941  fzto1st  33182  psgnfzto1st  33184  sgnsv  33239  sgnsval  33240  elrspunsn  33507  mvrvalind  33700  mplvrpmrhm  33709  psrmonmul  33712  psrmonmul2  33713  psrmonprod  33714  mplmonprod  33716  esplysply  33733  esplyfval1  33735  esplyfvaln  33736  esplyind  33737  smatfval  33958  1smat1  33967  ddeval1  34397  ddeval0  34398  eulerpartlemgvv  34539  signsvvfval  34741  signsvfn  34745  hashreprin  34783  circlemeth  34803  kur14  35417  ex-sategoelel  35622  mrsubrn  35714  prodeq12sdv  36419  itgeq12sdv  36420  cbvitgvw2  36449  cbvitgdavw  36482  cbvitgdavw2  36498  finxpeq1  37719  poimirlem5  37963  poimirlem6  37964  poimirlem7  37965  poimirlem8  37966  poimirlem10  37968  poimirlem11  37969  poimirlem12  37970  poimirlem15  37973  poimirlem16  37974  poimirlem17  37975  poimirlem18  37976  poimirlem19  37977  poimirlem20  37978  poimirlem21  37979  poimirlem22  37980  poimirlem23  37981  poimirlem27  37985  itg2addnclem  38009  itg2gt0cn  38013  ibladdnclem  38014  iblabsnclem  38021  ftc1anclem5  38035  ftc1anc  38039  ftc2nc  38040  frlmvscadiccat  42968  fiabv  42998  evlsbagval  43019  selvvvval  43035  fsuppind  43040  pw2f1ocnv  43486  flcidc  43619  cantnfresb  43773  refsum2cnlem1  45489  icccncfext  46336  fourierdlem112  46667  fourierswlem  46679  fouriersw  46680  etransclem1  46684  etransclem5  46688  etransclem17  46700  etransclem32  46715  etransclem41  46724  hoidmv1lelem2  47041  ovnhoi  47052  hspdifhsp  47065  hspmbl  47078  hoimbl  47080  ovnsubadd2  47095  suppmptcfin  48867  linc0scn0  48914  linc1  48916  lcoss  48927  el0ldep  48957