Theorem ifbid 4503

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  ifbieq1d  4504  ifbieq2d  4506  ifbieq12d  4508  ifbieq12d2  4514  ifan  4533  ifor  4534  rabsnif  4680  suppsnop  8120  resixpfo  8876  pw2f1olem  9011  unxpdomlem1  9158  cantnflem1d  9599  cantnflem1  9600  ssttrcl  9626  ttrclselem2  9637  dfac12lem1  10056  ttukeylem3  10423  2resupmax  13105  xaddval  13140  xmulcom  13183  xmulneg1  13186  repswswrd  14709  ccatco  14760  sgnval  15013  sumeq1  15614  sumsplit  15693  prodeq1f  15831  prodeq1  15832  rpnnen2lem1  16141  rpnnen2lem2  16142  rpnnen2lem10  16150  sadadd2lem2  16379  sadfval  16381  sadcp1  16384  sadadd2lem  16388  sadcom  16392  pcmpt  16822  pcmpt2  16823  pcfac  16829  prmrec  16852  ramcl  16959  acsfn  17584  setcepi  18014  mgmnsgrpex  18858  sgrpnmndex  18859  frgpup3lem  19708  dpjrid  19995  abvtrivd  20767  obsip  21678  uvcval  21742  uvcvval  21743  psrlidm  21919  psrridm  21920  psrascl  21936  mvrval  21939  mvrval2  21940  mvrf1  21943  mplmonmul  21993  mplcoe1  21994  mplcoe3  21995  mplcoe5  21997  evlslem3  22037  mhpsclcl  22092  psdfval  22103  psdmplcl  22107  psdmul  22111  psdmvr  22114  coe1tm  22217  coe1tmfv2  22219  gsummoncoe1  22254  mat1comp  22386  mamulid  22387  mamurid  22388  mat1ov  22394  mattpos1  22402  mat1dimid  22420  scmateALT  22458  scmatscm  22459  1mavmul  22494  marrepval  22508  marrepeval  22509  marepvval  22513  ma1repveval  22517  1marepvmarrepid  22521  mdetdiagid  22546  mdetunilem8  22565  mdetunilem9  22566  maducoeval  22585  maducoeval2  22586  madutpos  22588  madugsum  22589  minmar1val  22594  minmar1eval  22595  symgmatr01lem  22599  symgmatr01  22600  gsummatr01lem3  22603  gsummatr01lem4  22604  gsummatr01  22605  m2cpm  22687  m2cpminvid2lem  22700  decpmatid  22716  monmatcollpw  22725  mp2pm2mplem4  22755  chmatval  22775  fvmptnn04if  22795  fclsval  23954  tmsxpsval2  24485  dscmet  24518  dscopn  24519  ovolicc1  25475  ovolicc  25482  i1f1lem  25648  itg11  25650  i1fpos  25665  itg2uba  25702  itg2split  25708  itg2monolem1  25709  itg2cnlem1  25720  itg2cnlem2  25721  itg2cn  25722  ibllem  25723  isibl  25724  itgeq1f  25730  itgeq1fOLD  25731  itgeq1  25732  cbvitgv  25736  itgresr  25738  iblpos  25752  itgposval  25755  i1fibl  25767  ibladdlem  25779  iblabslem  25787  itgcn  25804  coe1termlem  26221  coe1term  26222  cxpval  26631  leibpilem2  26909  leibpi  26910  prmorcht  27146  sqff1o  27150  pclogsum  27184  dchr1  27226  dchr2sum  27242  sum2dchr  27243  lgsval  27270  lgsneg  27290  lgsdilem  27293  lgsdir2  27299  lgsdir  27301  dchrisum0flblem2  27478  dchrisum0flb  27479  ostth1  27602  partfun2  32757  mptprop  32779  sgnneg  32916  indval  32934  indfval  32937  prodindf  32946  indsn  32947  fzto1st  33187  psgnfzto1st  33189  sgnsv  33244  sgnsval  33245  elrspunsn  33512  mvrvalind  33705  mplvrpmrhm  33714  esplysply  33731  esplyind  33733  smatfval  33954  1smat1  33963  ddeval1  34393  ddeval0  34394  eulerpartlemgvv  34535  signsvvfval  34737  signsvfn  34741  hashreprin  34779  circlemeth  34799  kur14  35412  ex-sategoelel  35617  mrsubrn  35709  prodeq12sdv  36414  itgeq12sdv  36415  cbvitgvw2  36444  cbvitgdavw  36477  cbvitgdavw2  36493  finxpeq1  37593  poimirlem5  37828  poimirlem6  37829  poimirlem7  37830  poimirlem8  37831  poimirlem10  37833  poimirlem11  37834  poimirlem12  37835  poimirlem15  37838  poimirlem16  37839  poimirlem17  37840  poimirlem18  37841  poimirlem19  37842  poimirlem20  37843  poimirlem21  37844  poimirlem22  37845  poimirlem23  37846  poimirlem27  37850  itg2addnclem  37874  itg2gt0cn  37878  ibladdnclem  37879  iblabsnclem  37886  ftc1anclem5  37900  ftc1anc  37904  ftc2nc  37905  frlmvscadiccat  42782  fiabv  42812  evlsbagval  42833  selvvvval  42849  fsuppind  42854  pw2f1ocnv  43300  flcidc  43433  cantnfresb  43587  refsum2cnlem1  45303  icccncfext  46152  fourierdlem112  46483  fourierswlem  46495  fouriersw  46496  etransclem1  46500  etransclem5  46504  etransclem17  46516  etransclem32  46531  etransclem41  46540  hoidmv1lelem2  46857  ovnhoi  46868  hspdifhsp  46881  hspmbl  46894  hoimbl  46896  ovnsubadd2  46911  suppmptcfin  48643  linc0scn0  48690  linc1  48692  lcoss  48703  el0ldep  48733