Theorem ifbid 4516

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ifcif 4492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-if 4493

This theorem is referenced by:  ifbieq1d  4517  ifbieq2d  4519  ifbieq12d  4521  ifbieq12d2  4527  ifan  4546  ifor  4547  rabsnif  4694  suppsnop  8174  resixpfo  8934  pw2f1olem  9069  unxpdomlem1  9216  cantnflem1d  9657  cantnflem1  9658  ssttrcl  9684  ttrclselem2  9695  dfac12lem1  10127  ttukeylem3  10495  indval  12221  indfval  12225  2resupmax  13214  xaddval  13249  xmulcom  13292  xmulneg1  13295  repswswrd  14821  ccatco  14872  sgnval  15125  sgnneg  15137  sumeq1  15740  sumsplit  15819  prodeq1f  15960  prodeq1  15961  rpnnen2lem1  16270  rpnnen2lem2  16271  rpnnen2lem10  16279  sadadd2lem2  16508  sadfval  16510  sadcp1  16513  sadadd2lem  16517  sadcom  16521  pcmpt  16952  pcmpt2  16953  pcfac  16959  prmrec  16982  ramcl  17089  acsfn  17715  setcepi  18145  mgmnsgrpex  18993  sgrpnmndex  18994  frgpup3lem  19847  dpjrid  20134  abvtrivd  20913  obsip  21840  uvcval  21904  uvcvval  21905  psrlidm  22080  psrridm  22081  psrascl  22097  mvrval  22100  mvrval2  22101  mvrf1  22104  mplmonmul  22156  mplcoe1  22157  mplcoe3  22158  mplcoe5  22160  evlslem3  22200  selvvvval  22262  mhpsclcl  22279  psdfval  22290  psdmplcl  22294  psdmul  22298  psdmvr  22301  coe1tm  22403  coe1tmfv2  22405  gsummoncoe1  22437  mat1comp  22566  mamulid  22567  mamurid  22568  mat1ov  22574  mattpos1  22582  mat1dimid  22600  scmateALT  22638  scmatscm  22639  1mavmul  22674  marrepval  22688  marrepeval  22689  marepvval  22693  ma1repveval  22697  1marepvmarrepid  22701  mdetdiagid  22726  mdetunilem8  22745  mdetunilem9  22746  maducoeval  22765  maducoeval2  22766  madutpos  22768  madugsum  22769  minmar1val  22774  minmar1eval  22775  symgmatr01lem  22779  symgmatr01  22780  gsummatr01lem3  22783  gsummatr01lem4  22784  gsummatr01  22785  m2cpm  22867  m2cpminvid2lem  22880  decpmatid  22896  monmatcollpw  22905  mp2pm2mplem4  22935  chmatval  22955  fvmptnn04if  22975  fclsval  24134  tmsxpsval2  24665  dscmet  24698  dscopn  24699  ovolicc1  25644  ovolicc  25651  i1f1lem  25817  itg11  25819  i1fpos  25834  itg2uba  25871  itg2split  25877  itg2monolem1  25878  itg2cnlem1  25889  itg2cnlem2  25890  itg2cn  25891  ibllem  25892  isibl  25893  itgeq1f  25899  itgeq1fOLD  25900  itgeq1  25901  cbvitgv  25905  itgresr  25907  iblpos  25921  itgposval  25924  i1fibl  25936  ibladdlem  25948  iblabslem  25956  itgcn  25973  coe1termlem  26384  coe1term  26385  cxpval  26795  leibpilem2  27072  leibpi  27073  prmorcht  27308  sqff1o  27312  pclogsum  27345  dchr1  27387  dchr2sum  27403  sum2dchr  27404  lgsval  27431  lgsneg  27451  lgsdilem  27454  lgsdir2  27460  lgsdir  27462  dchrisum0flblem2  27639  dchrisum0flb  27640  ostth1  27763  partfun2  32962  mptprop  32984  prodindf  33123  indsn  33124  fzto1st  33364  psgnfzto1st  33366  sgnsv  33421  sgnsval  33422  elrspunsn  33681  mvrvalind  33873  mplvrpmrhm  33882  psrmonmul  33885  psrmonmul2  33886  psrmonprod  33887  mplmonprod  33889  esplysply  33906  esplyfval1  33908  esplyfvaln  33909  esplyind  33910  smatfval  34130  1smat1  34139  ddeval1  34569  ddeval0  34570  eulerpartlemgvv  34711  signsvvfval  34910  signsvfn  34914  hashreprin  34952  circlemeth  34972  kur14  35641  ex-sategoelel  35846  mrsubrn  35938  prodeq12sdv  36653  itgeq12sdv  36654  cbvitgvw2  36683  cbvitgdavw  36716  cbvitgdavw2  36732  finxpeq1  37954  poimirlem5  38198  poimirlem6  38199  poimirlem7  38200  poimirlem8  38201  poimirlem10  38203  poimirlem11  38204  poimirlem12  38205  poimirlem15  38208  poimirlem16  38209  poimirlem17  38210  poimirlem18  38211  poimirlem19  38212  poimirlem20  38213  poimirlem21  38214  poimirlem22  38215  poimirlem23  38216  poimirlem27  38220  itg2addnclem  38244  itg2gt0cn  38248  ibladdnclem  38249  iblabsnclem  38256  ftc1anclem5  38270  ftc1anc  38274  ftc2nc  38275  frlmvscadiccat  43204  fiabv  43230  evlsbagval  43244  fsuppind  43248  pw2f1ocnv  43690  flcidc  43823  cantnfresb  43977  refsum2cnlem1  45683  icccncfext  46527  fourierdlem112  46858  fourierswlem  46870  fouriersw  46871  etransclem1  46875  etransclem5  46879  etransclem17  46891  etransclem32  46906  etransclem41  46915  hoidmv1lelem2  47232  ovnhoi  47243  hspdifhsp  47256  hspmbl  47269  hoimbl  47271  ovnsubadd2  47286  suppmptcfin  49075  linc0scn0  49122  linc1  49124  lcoss  49135  el0ldep  49165