Theorem ifbid 4553

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-if 4531

This theorem is referenced by:  ifbieq1d  4554  ifbieq2d  4556  ifbieq12d  4558  ifbieq12d2  4564  ifan  4583  ifor  4584  rabsnif  4729  suppsnop  8183  resixpfo  8955  pw2f1olem  9104  unxpdomlem1  9278  cantnflem1d  9718  cantnflem1  9719  ssttrcl  9745  ttrclselem2  9756  dfac12lem1  10173  ttukeylem3  10541  2resupmax  13207  xaddval  13242  xmulcom  13285  xmulneg1  13288  repswswrd  14775  ccatco  14827  sgnval  15076  sumeq1  15676  sumsplit  15755  prodeq1f  15893  rpnnen2lem1  16199  rpnnen2lem2  16200  rpnnen2lem10  16208  sadadd2lem2  16433  sadfval  16435  sadcp1  16438  sadadd2lem  16442  sadcom  16446  pcmpt  16869  pcmpt2  16870  pcfac  16876  prmrec  16899  ramcl  17006  acsfn  17647  setcepi  18085  mgmnsgrpex  18896  sgrpnmndex  18897  frgpup3lem  19749  dpjrid  20036  abvtrivd  20737  obsip  21677  uvcval  21741  uvcvval  21742  psrlidm  21929  psrridm  21930  psrascl  21946  mvrval  21949  mvrval2  21950  mvrf1  21953  mplmonmul  22001  mplcoe1  22002  mplcoe3  22003  mplcoe5  22005  evlslem3  22053  mhpsclcl  22099  psdfval  22110  psdmplcl  22114  psdmul  22118  coe1tm  22222  coe1tmfv2  22224  gsummoncoe1  22257  mat1comp  22391  mamulid  22392  mamurid  22393  mat1ov  22399  mattpos1  22407  mat1dimid  22425  scmateALT  22463  scmatscm  22464  1mavmul  22499  marrepval  22513  marrepeval  22514  marepvval  22518  ma1repveval  22522  1marepvmarrepid  22526  mdetdiagid  22551  mdetunilem8  22570  mdetunilem9  22571  maducoeval  22590  maducoeval2  22591  madutpos  22593  madugsum  22594  minmar1val  22599  minmar1eval  22600  symgmatr01lem  22604  symgmatr01  22605  gsummatr01lem3  22608  gsummatr01lem4  22609  gsummatr01  22610  m2cpm  22692  m2cpminvid2lem  22705  decpmatid  22721  monmatcollpw  22730  mp2pm2mplem4  22760  chmatval  22780  fvmptnn04if  22800  fclsval  23961  tmsxpsval2  24497  dscmet  24530  dscopn  24531  ovolicc1  25494  ovolicc  25501  i1f1lem  25667  itg11  25669  i1fpos  25685  itg2uba  25722  itg2split  25728  itg2monolem1  25729  itg2cnlem1  25740  itg2cnlem2  25741  itg2cn  25742  ibllem  25743  isibl  25744  itgeq1f  25750  itgresr  25757  iblpos  25771  itgposval  25774  i1fibl  25786  ibladdlem  25798  iblabslem  25806  itgcn  25823  coe1termlem  26242  coe1term  26243  cxpval  26648  leibpilem2  26923  leibpi  26924  prmorcht  27160  sqff1o  27164  pclogsum  27198  dchr1  27240  dchr2sum  27256  sum2dchr  27257  lgsval  27284  lgsneg  27304  lgsdilem  27307  lgsdir2  27313  lgsdir  27315  dchrisum0flblem2  27492  dchrisum0flb  27493  ostth1  27616  mptprop  32565  fzto1st  32921  psgnfzto1st  32923  sgnsv  32978  sgnsval  32979  elrspunsn  33246  smatfval  33529  1smat1  33538  indval  33765  indfval  33768  prodindf  33775  ddeval1  33986  ddeval0  33987  eulerpartlemgvv  34129  sgnneg  34293  signsvvfval  34343  signsvfn  34347  hashreprin  34385  circlemeth  34405  kur14  34959  ex-sategoelel  35164  mrsubrn  35256  finxpeq1  36998  poimirlem5  37231  poimirlem6  37232  poimirlem7  37233  poimirlem8  37234  poimirlem10  37236  poimirlem11  37237  poimirlem12  37238  poimirlem15  37241  poimirlem16  37242  poimirlem17  37243  poimirlem18  37244  poimirlem19  37245  poimirlem20  37246  poimirlem21  37247  poimirlem22  37248  poimirlem23  37249  poimirlem27  37253  itg2addnclem  37277  itg2gt0cn  37281  ibladdnclem  37282  iblabsnclem  37289  ftc1anclem5  37303  ftc1anc  37307  ftc2nc  37308  metakunt11  41803  metakunt32  41824  frlmvscadiccat  41886  evlsbagval  41936  selvvvval  41955  fsuppind  41960  pw2f1ocnv  42602  flcidc  42742  cantnfresb  42897  refsum2cnlem1  44543  icccncfext  45415  fourierdlem112  45746  fourierswlem  45758  fouriersw  45759  etransclem1  45763  etransclem5  45767  etransclem17  45779  etransclem32  45794  etransclem41  45803  hoidmv1lelem2  46120  ovnhoi  46131  hspdifhsp  46144  hspmbl  46157  hoimbl  46159  ovnsubadd2  46174  suppmptcfin  47631  linc0scn0  47679  linc1  47681  lcoss  47692  el0ldep  47722