Theorem ifbid 4513

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ifcif 4489

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4490

This theorem is used by:  ifbieq1d  4514  ifbieq2d  4516  ifbieq12d  4518  ifbieq12d2  4524  ifan  4543  ifor  4544  rabsnif  4691  suppsnop  8180  resixpfo  8940  pw2f1olem  9076  unxpdomlem1  9223  cantnflem1d  9664  cantnflem1  9665  ssttrcl  9691  ttrclselem2  9702  dfac12lem1  10143  ttukeylem3  10510  indval  12238  indfval  12242  2resupmax  13232  xaddval  13267  xmulcom  13310  xmulneg1  13313  repswswrd  14847  ccatco  14898  sgnval  15151  sgnneg  15163  sumeq1  15766  sumsplit  15844  prodeq1f  15985  prodeq1  15986  rpnnen2lem1  16294  rpnnen2lem2  16295  rpnnen2lem10  16303  sadadd2lem2  16532  sadfval  16534  sadcp1  16537  sadadd2lem  16541  sadcom  16545  pcmpt  16976  pcmpt2  16977  pcfac  16983  prmrec  17006  ramcl  17113  acsfn  17739  setcepi  18169  mgmnsgrpex  19032  sgrpnmndex  19033  frgpup3lem  19893  dpjrid  20180  abvtrivd  20987  obsip  21923  uvcval  21987  uvcvval  21988  psrlidm  22163  psrridm  22164  psrascl  22180  mvrval  22183  mvrval2  22184  mvrf1  22187  mplmonmul  22239  mplcoe1  22240  mplcoe3  22241  mplcoe5  22243  evlslem3  22283  selvvvval  22345  mhpsclcl  22362  psdfval  22373  psdmplcl  22377  psdmul  22381  psdmvr  22384  coe1tm  22486  coe1tmfv2  22488  gsummoncoe1  22520  mat1comp  22649  mamulid  22650  mamurid  22651  mat1ov  22657  mattpos1  22665  mat1dimid  22683  scmateALT  22721  scmatscm  22722  1mavmul  22757  marrepval  22771  marrepeval  22772  marepvval  22776  ma1repveval  22780  1marepvmarrepid  22784  mdetdiagid  22809  mdetunilem8  22828  mdetunilem9  22829  maducoeval  22848  maducoeval2  22849  madutpos  22851  madugsum  22852  minmar1val  22857  minmar1eval  22858  symgmatr01lem  22862  symgmatr01  22863  gsummatr01lem3  22866  gsummatr01lem4  22867  gsummatr01  22868  m2cpm  22950  m2cpminvid2lem  22963  decpmatid  22979  monmatcollpw  22988  mp2pm2mplem4  23018  chmatval  23038  fvmptnn04if  23058  fclsval  24218  tmsxpsval2  24749  dscmet  24782  dscopn  24783  ovolicc1  25728  ovolicc  25735  i1f1lem  25901  itg11  25903  i1fpos  25918  itg2uba  25955  itg2split  25961  itg2monolem1  25962  itg2cnlem1  25973  itg2cnlem2  25974  itg2cn  25975  ibllem  25976  isibl  25977  itgeq1f  25983  itgeq1fOLD  25984  itgeq1  25985  cbvitgv  25989  itgresr  25991  iblpos  26005  itgposval  26008  i1fibl  26020  ibladdlem  26032  iblabslem  26040  itgcn  26057  coe1termlem  26468  coe1term  26469  cxpval  26882  leibpilem2  27159  leibpi  27160  prmorcht  27395  sqff1o  27399  pclogsum  27432  dchr1  27474  dchr2sum  27490  sum2dchr  27491  lgsval  27518  lgsneg  27538  lgsdilem  27541  lgsdir2  27547  lgsdir  27549  dchrisum0flblem2  27726  dchrisum0flb  27727  ostth1  27850  partfun2  33094  mptprop  33116  prodindf  33254  indsn  33255  fzto1st  33489  psgnfzto1st  33491  sgnsv  33546  sgnsval  33547  elrspunsn  33803  mvrvalind  33994  mplvrpmrhm  34003  psrmonmul  34006  psrmonmul2  34007  psrmonprod  34008  mplmonprod  34010  esplysply  34027  esplyfval1  34029  esplyfvaln  34030  esplyind  34031  smatfval  34251  1smat1  34260  ddeval1  34691  ddeval0  34692  eulerpartlemgvv  34833  signsvvfval  35032  signsvfn  35036  hashreprin  35074  circlemeth  35094  kur14  35747  ex-sategoelel  35952  mrsubrn  36044  prodeq12sdv  36789  itgeq12sdv  36790  cbvitgvw2  36819  cbvitgdavw  36852  cbvitgdavw2  36868  finxpeq1  38091  poimirlem5  38335  poimirlem6  38336  poimirlem7  38337  poimirlem8  38338  poimirlem10  38340  poimirlem11  38341  poimirlem12  38342  poimirlem15  38345  poimirlem16  38346  poimirlem17  38347  poimirlem18  38348  poimirlem19  38349  poimirlem20  38350  poimirlem21  38351  poimirlem22  38352  poimirlem23  38353  poimirlem27  38357  itg2addnclem  38381  itg2gt0cn  38385  ibladdnclem  38386  iblabsnclem  38393  ftc1anclem5  38407  ftc1anc  38411  ftc2nc  38412  frlmvscadiccat  43340  fiabv  43364  evlsbagval  43378  fsuppind  43382  pw2f1ocnv  43824  flcidc  43957  cantnfresb  44111  refsum2cnlem1  45817  icccncfext  46661  fourierdlem112  46992  fourierswlem  47004  fouriersw  47005  etransclem1  47009  etransclem5  47013  etransclem17  47025  etransclem32  47040  etransclem41  47049  hoidmv1lelem2  47366  ovnhoi  47377  hspdifhsp  47390  hspmbl  47403  hoimbl  47405  ovnsubadd2  47420  suppmptcfin  49215  linc0scn0  49262  linc1  49264  lcoss  49275  el0ldep  49305