Theorem ifbid 4482

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ifcif 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-if 4460

This theorem is referenced by:  ifbieq1d  4483  ifbieq2d  4485  ifbieq12d  4487  ifbieq12d2  4493  ifan  4512  ifor  4513  rabsnif  4659  suppsnop  7994  resixpfo  8724  pw2f1olem  8863  unxpdomlem1  9027  cantnflem1d  9446  cantnflem1  9447  ssttrcl  9473  ttrclselem2  9484  dfac12lem1  9899  ttukeylem3  10267  2resupmax  12922  xaddval  12957  xmulcom  13000  xmulneg1  13003  repswswrd  14497  ccatco  14548  sgnval  14799  sumeq1  15400  sumsplit  15480  prodeq1f  15618  rpnnen2lem1  15923  rpnnen2lem2  15924  rpnnen2lem10  15932  sadadd2lem2  16157  sadfval  16159  sadcp1  16162  sadadd2lem  16166  sadcom  16170  pcmpt  16593  pcmpt2  16594  pcfac  16600  prmrec  16623  ramcl  16730  acsfn  17368  setcepi  17803  mgmnsgrpex  18570  sgrpnmndex  18571  frgpup3lem  19383  dpjrid  19665  abvtrivd  20100  obsip  20928  uvcval  20992  uvcvval  20993  psrlidm  21172  psrridm  21173  mvrval  21190  mvrval2  21191  mvrf1  21194  mplmonmul  21237  mplcoe1  21238  mplcoe3  21239  mplcoe5  21241  evlslem3  21290  mhpsclcl  21337  coe1tm  21444  coe1tmfv2  21446  gsummoncoe1  21475  mat1comp  21589  mamulid  21590  mamurid  21591  mat1ov  21597  mattpos1  21605  mat1dimid  21623  scmateALT  21661  scmatscm  21662  1mavmul  21697  marrepval  21711  marrepeval  21712  marepvval  21716  ma1repveval  21720  1marepvmarrepid  21724  mdetdiagid  21749  mdetunilem8  21768  mdetunilem9  21769  maducoeval  21788  maducoeval2  21789  madutpos  21791  madugsum  21792  minmar1val  21797  minmar1eval  21798  symgmatr01lem  21802  symgmatr01  21803  gsummatr01lem3  21806  gsummatr01lem4  21807  gsummatr01  21808  m2cpm  21890  m2cpminvid2lem  21903  decpmatid  21919  monmatcollpw  21928  mp2pm2mplem4  21958  chmatval  21978  fvmptnn04if  21998  fclsval  23159  tmsxpsval2  23695  dscmet  23728  dscopn  23729  ovolicc1  24680  ovolicc  24687  i1f1lem  24853  itg11  24855  i1fpos  24871  itg2uba  24908  itg2split  24914  itg2monolem1  24915  itg2cnlem1  24926  itg2cnlem2  24927  itg2cn  24928  ibllem  24929  isibl  24930  itgeq1f  24936  itgresr  24943  iblpos  24957  itgposval  24960  i1fibl  24972  ibladdlem  24984  iblabslem  24992  itgcn  25009  coe1termlem  25419  coe1term  25420  cxpval  25819  leibpilem2  26091  leibpi  26092  prmorcht  26327  sqff1o  26331  pclogsum  26363  dchr1  26405  dchr2sum  26421  sum2dchr  26422  lgsval  26449  lgsneg  26469  lgsdilem  26472  lgsdir2  26478  lgsdir  26480  dchrisum0flblem2  26657  dchrisum0flb  26658  ostth1  26781  mptprop  31031  fzto1st  31370  psgnfzto1st  31372  sgnsv  31427  sgnsval  31428  smatfval  31745  1smat1  31754  indval  31981  indfval  31984  prodindf  31991  ddeval1  32202  ddeval0  32203  eulerpartlemgvv  32343  sgnneg  32507  signsvvfval  32557  signsvfn  32561  hashreprin  32600  circlemeth  32620  kur14  33178  ex-sategoelel  33383  mrsubrn  33475  finxpeq1  35557  poimirlem5  35782  poimirlem6  35783  poimirlem7  35784  poimirlem8  35785  poimirlem10  35787  poimirlem11  35788  poimirlem12  35789  poimirlem15  35792  poimirlem16  35793  poimirlem17  35794  poimirlem18  35795  poimirlem19  35796  poimirlem20  35797  poimirlem21  35798  poimirlem22  35799  poimirlem23  35800  poimirlem27  35804  itg2addnclem  35828  itg2gt0cn  35832  ibladdnclem  35833  iblabsnclem  35840  ftc1anclem5  35854  ftc1anc  35858  ftc2nc  35859  metakunt11  40135  metakunt32  40156  frlmvscadiccat  40237  evlsbagval  40275  fsuppind  40279  mhphf  40285  pw2f1ocnv  40859  flcidc  40999  refsum2cnlem1  42580  icccncfext  43428  fourierdlem112  43759  fourierswlem  43771  fouriersw  43772  etransclem1  43776  etransclem5  43780  etransclem17  43792  etransclem32  43807  etransclem41  43816  hoidmv1lelem2  44130  ovnhoi  44141  hspdifhsp  44154  hspmbl  44167  hoimbl  44169  ovnsubadd2  44184  suppmptcfin  45715  linc0scn0  45764  linc1  45766  lcoss  45777  el0ldep  45807