Theorem ifbid 4479

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ifcif 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-if 4456

This theorem is referenced by:  ifbieq1d  4480  ifbieq2d  4482  ifbieq12d  4484  ifbieq12d2  4490  ifan  4509  ifor  4510  rabsnif  4656  suppsnop  8119  resixpfo  8875  pw2f1olem  9010  unxpdomlem1  9157  cantnflem1d  9601  cantnflem1  9602  ssttrcl  9628  ttrclselem2  9639  dfac12lem1  10058  ttukeylem3  10425  indval  12154  indfval  12158  2resupmax  13132  xaddval  13167  xmulcom  13210  xmulneg1  13213  repswswrd  14738  ccatco  14789  sgnval  15042  sumeq1  15643  sumsplit  15722  prodeq1f  15863  prodeq1  15864  rpnnen2lem1  16173  rpnnen2lem2  16174  rpnnen2lem10  16182  sadadd2lem2  16411  sadfval  16413  sadcp1  16416  sadadd2lem  16420  sadcom  16424  pcmpt  16855  pcmpt2  16856  pcfac  16862  prmrec  16885  ramcl  16992  acsfn  17617  setcepi  18047  mgmnsgrpex  18894  sgrpnmndex  18895  frgpup3lem  19744  dpjrid  20031  abvtrivd  20805  obsip  21697  uvcval  21761  uvcvval  21762  psrlidm  21937  psrridm  21938  psrascl  21954  mvrval  21957  mvrval2  21958  mvrf1  21961  mplmonmul  22013  mplcoe1  22014  mplcoe3  22015  mplcoe5  22017  evlslem3  22057  selvvvval  22119  mhpsclcl  22136  psdfval  22147  psdmplcl  22151  psdmul  22155  psdmvr  22158  coe1tm  22260  coe1tmfv2  22262  gsummoncoe1  22295  mat1comp  22424  mamulid  22425  mamurid  22426  mat1ov  22432  mattpos1  22440  mat1dimid  22458  scmateALT  22496  scmatscm  22497  1mavmul  22532  marrepval  22546  marrepeval  22547  marepvval  22551  ma1repveval  22555  1marepvmarrepid  22559  mdetdiagid  22584  mdetunilem8  22603  mdetunilem9  22604  maducoeval  22623  maducoeval2  22624  madutpos  22626  madugsum  22627  minmar1val  22632  minmar1eval  22633  symgmatr01lem  22637  symgmatr01  22638  gsummatr01lem3  22641  gsummatr01lem4  22642  gsummatr01  22643  m2cpm  22725  m2cpminvid2lem  22738  decpmatid  22754  monmatcollpw  22763  mp2pm2mplem4  22793  chmatval  22813  fvmptnn04if  22833  fclsval  23992  tmsxpsval2  24523  dscmet  24556  dscopn  24557  ovolicc1  25502  ovolicc  25509  i1f1lem  25675  itg11  25677  i1fpos  25692  itg2uba  25729  itg2split  25735  itg2monolem1  25736  itg2cnlem1  25747  itg2cnlem2  25748  itg2cn  25749  ibllem  25750  isibl  25751  itgeq1f  25757  itgeq1fOLD  25758  itgeq1  25759  cbvitgv  25763  itgresr  25765  iblpos  25779  itgposval  25782  i1fibl  25794  ibladdlem  25806  iblabslem  25814  itgcn  25831  coe1termlem  26242  coe1term  26243  cxpval  26647  leibpilem2  26924  leibpi  26925  prmorcht  27160  sqff1o  27164  pclogsum  27197  dchr1  27239  dchr2sum  27255  sum2dchr  27256  lgsval  27283  lgsneg  27303  lgsdilem  27306  lgsdir2  27312  lgsdir  27314  dchrisum0flblem2  27491  dchrisum0flb  27492  ostth1  27615  partfun2  32769  mptprop  32791  sgnneg  32926  prodindf  32942  indsn  32943  fzto1st  33185  psgnfzto1st  33187  sgnsv  33242  sgnsval  33243  elrspunsn  33513  mvrvalind  33731  mplvrpmrhm  33740  psrmonmul  33743  psrmonmul2  33744  psrmonprod  33745  mplmonprod  33747  esplysply  33764  esplyfval1  33766  esplyfvaln  33767  esplyind  33768  smatfval  33988  1smat1  33997  ddeval1  34427  ddeval0  34428  eulerpartlemgvv  34569  signsvvfval  34771  signsvfn  34775  hashreprin  34813  circlemeth  34833  kur14  35453  ex-sategoelel  35658  mrsubrn  35750  prodeq12sdv  36455  itgeq12sdv  36456  cbvitgvw2  36485  cbvitgdavw  36518  cbvitgdavw2  36534  finxpeq1  37757  poimirlem5  38001  poimirlem6  38002  poimirlem7  38003  poimirlem8  38004  poimirlem10  38006  poimirlem11  38007  poimirlem12  38008  poimirlem15  38011  poimirlem16  38012  poimirlem17  38013  poimirlem18  38014  poimirlem19  38015  poimirlem20  38016  poimirlem21  38017  poimirlem22  38018  poimirlem23  38019  poimirlem27  38023  itg2addnclem  38047  itg2gt0cn  38051  ibladdnclem  38052  iblabsnclem  38059  ftc1anclem5  38073  ftc1anc  38077  ftc2nc  38078  frlmvscadiccat  43005  fiabv  43031  evlsbagval  43045  fsuppind  43049  pw2f1ocnv  43491  flcidc  43624  cantnfresb  43778  refsum2cnlem1  45494  icccncfext  46338  fourierdlem112  46669  fourierswlem  46681  fouriersw  46682  etransclem1  46686  etransclem5  46690  etransclem17  46702  etransclem32  46717  etransclem41  46726  hoidmv1lelem2  47043  ovnhoi  47054  hspdifhsp  47067  hspmbl  47080  hoimbl  47082  ovnsubadd2  47097  suppmptcfin  48875  linc0scn0  48922  linc1  48924  lcoss  48935  el0ldep  48965