Theorem ifbid 4524

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  ifbieq1d  4525  ifbieq2d  4527  ifbieq12d  4529  ifbieq12d2  4535  ifan  4554  ifor  4555  rabsnif  4699  suppsnop  8177  resixpfo  8950  pw2f1olem  9090  unxpdomlem1  9258  cantnflem1d  9702  cantnflem1  9703  ssttrcl  9729  ttrclselem2  9740  dfac12lem1  10158  ttukeylem3  10525  2resupmax  13204  xaddval  13239  xmulcom  13282  xmulneg1  13285  repswswrd  14802  ccatco  14854  sgnval  15107  sumeq1  15705  sumsplit  15784  prodeq1f  15922  prodeq1  15923  rpnnen2lem1  16232  rpnnen2lem2  16233  rpnnen2lem10  16241  sadadd2lem2  16469  sadfval  16471  sadcp1  16474  sadadd2lem  16478  sadcom  16482  pcmpt  16912  pcmpt2  16913  pcfac  16919  prmrec  16942  ramcl  17049  acsfn  17671  setcepi  18101  mgmnsgrpex  18909  sgrpnmndex  18910  frgpup3lem  19758  dpjrid  20045  abvtrivd  20792  obsip  21681  uvcval  21745  uvcvval  21746  psrlidm  21922  psrridm  21923  psrascl  21939  mvrval  21942  mvrval2  21943  mvrf1  21946  mplmonmul  21994  mplcoe1  21995  mplcoe3  21996  mplcoe5  21998  evlslem3  22038  mhpsclcl  22085  psdfval  22096  psdmplcl  22100  psdmul  22104  psdmvr  22107  coe1tm  22210  coe1tmfv2  22212  gsummoncoe1  22246  mat1comp  22378  mamulid  22379  mamurid  22380  mat1ov  22386  mattpos1  22394  mat1dimid  22412  scmateALT  22450  scmatscm  22451  1mavmul  22486  marrepval  22500  marrepeval  22501  marepvval  22505  ma1repveval  22509  1marepvmarrepid  22513  mdetdiagid  22538  mdetunilem8  22557  mdetunilem9  22558  maducoeval  22577  maducoeval2  22578  madutpos  22580  madugsum  22581  minmar1val  22586  minmar1eval  22587  symgmatr01lem  22591  symgmatr01  22592  gsummatr01lem3  22595  gsummatr01lem4  22596  gsummatr01  22597  m2cpm  22679  m2cpminvid2lem  22692  decpmatid  22708  monmatcollpw  22717  mp2pm2mplem4  22747  chmatval  22767  fvmptnn04if  22787  fclsval  23946  tmsxpsval2  24478  dscmet  24511  dscopn  24512  ovolicc1  25469  ovolicc  25476  i1f1lem  25642  itg11  25644  i1fpos  25659  itg2uba  25696  itg2split  25702  itg2monolem1  25703  itg2cnlem1  25714  itg2cnlem2  25715  itg2cn  25716  ibllem  25717  isibl  25718  itgeq1f  25724  itgeq1fOLD  25725  itgeq1  25726  cbvitgv  25730  itgresr  25732  iblpos  25746  itgposval  25749  i1fibl  25761  ibladdlem  25773  iblabslem  25781  itgcn  25798  coe1termlem  26215  coe1term  26216  cxpval  26625  leibpilem2  26903  leibpi  26904  prmorcht  27140  sqff1o  27144  pclogsum  27178  dchr1  27220  dchr2sum  27236  sum2dchr  27237  lgsval  27264  lgsneg  27284  lgsdilem  27287  lgsdir2  27293  lgsdir  27295  dchrisum0flblem2  27472  dchrisum0flb  27473  ostth1  27596  mptprop  32675  sgnneg  32812  indval  32830  indfval  32833  prodindf  32840  fzto1st  33114  psgnfzto1st  33116  sgnsv  33171  sgnsval  33172  elrspunsn  33444  smatfval  33826  1smat1  33835  ddeval1  34265  ddeval0  34266  eulerpartlemgvv  34408  signsvvfval  34610  signsvfn  34614  hashreprin  34652  circlemeth  34672  kur14  35238  ex-sategoelel  35443  mrsubrn  35535  prodeq12sdv  36236  itgeq12sdv  36237  cbvitgvw2  36266  cbvitgdavw  36299  cbvitgdavw2  36315  finxpeq1  37404  poimirlem5  37649  poimirlem6  37650  poimirlem7  37651  poimirlem8  37652  poimirlem10  37654  poimirlem11  37655  poimirlem12  37656  poimirlem15  37659  poimirlem16  37660  poimirlem17  37661  poimirlem18  37662  poimirlem19  37663  poimirlem20  37664  poimirlem21  37665  poimirlem22  37666  poimirlem23  37667  poimirlem27  37671  itg2addnclem  37695  itg2gt0cn  37699  ibladdnclem  37700  iblabsnclem  37707  ftc1anclem5  37721  ftc1anc  37725  ftc2nc  37726  metakunt11  42228  metakunt32  42249  frlmvscadiccat  42529  fiabv  42559  evlsbagval  42589  selvvvval  42608  fsuppind  42613  pw2f1ocnv  43061  flcidc  43194  cantnfresb  43348  refsum2cnlem1  45061  icccncfext  45916  fourierdlem112  46247  fourierswlem  46259  fouriersw  46260  etransclem1  46264  etransclem5  46268  etransclem17  46280  etransclem32  46295  etransclem41  46304  hoidmv1lelem2  46621  ovnhoi  46632  hspdifhsp  46645  hspmbl  46658  hoimbl  46660  ovnsubadd2  46675  suppmptcfin  48351  linc0scn0  48399  linc1  48401  lcoss  48412  el0ldep  48442