Theorem ifbid 4552

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  ifbieq1d  4553  ifbieq2d  4555  ifbieq12d  4557  ifbieq12d2  4563  ifan  4582  ifor  4583  rabsnif  4728  suppsnop  8163  resixpfo  8930  pw2f1olem  9076  unxpdomlem1  9250  cantnflem1d  9683  cantnflem1  9684  ssttrcl  9710  ttrclselem2  9721  dfac12lem1  10138  ttukeylem3  10506  2resupmax  13167  xaddval  13202  xmulcom  13245  xmulneg1  13248  repswswrd  14734  ccatco  14786  sgnval  15035  sumeq1  15635  sumsplit  15714  prodeq1f  15852  rpnnen2lem1  16157  rpnnen2lem2  16158  rpnnen2lem10  16166  sadadd2lem2  16391  sadfval  16393  sadcp1  16396  sadadd2lem  16400  sadcom  16404  pcmpt  16825  pcmpt2  16826  pcfac  16832  prmrec  16855  ramcl  16962  acsfn  17603  setcepi  18038  mgmnsgrpex  18812  sgrpnmndex  18813  frgpup3lem  19645  dpjrid  19932  abvtrivd  20448  obsip  21276  uvcval  21340  uvcvval  21341  psrlidm  21523  psrridm  21524  mvrval  21541  mvrval2  21542  mvrf1  21545  mplmonmul  21591  mplcoe1  21592  mplcoe3  21593  mplcoe5  21595  evlslem3  21643  mhpsclcl  21690  coe1tm  21795  coe1tmfv2  21797  gsummoncoe1  21828  mat1comp  21942  mamulid  21943  mamurid  21944  mat1ov  21950  mattpos1  21958  mat1dimid  21976  scmateALT  22014  scmatscm  22015  1mavmul  22050  marrepval  22064  marrepeval  22065  marepvval  22069  ma1repveval  22073  1marepvmarrepid  22077  mdetdiagid  22102  mdetunilem8  22121  mdetunilem9  22122  maducoeval  22141  maducoeval2  22142  madutpos  22144  madugsum  22145  minmar1val  22150  minmar1eval  22151  symgmatr01lem  22155  symgmatr01  22156  gsummatr01lem3  22159  gsummatr01lem4  22160  gsummatr01  22161  m2cpm  22243  m2cpminvid2lem  22256  decpmatid  22272  monmatcollpw  22281  mp2pm2mplem4  22311  chmatval  22331  fvmptnn04if  22351  fclsval  23512  tmsxpsval2  24048  dscmet  24081  dscopn  24082  ovolicc1  25033  ovolicc  25040  i1f1lem  25206  itg11  25208  i1fpos  25224  itg2uba  25261  itg2split  25267  itg2monolem1  25268  itg2cnlem1  25279  itg2cnlem2  25280  itg2cn  25281  ibllem  25282  isibl  25283  itgeq1f  25289  itgresr  25296  iblpos  25310  itgposval  25313  i1fibl  25325  ibladdlem  25337  iblabslem  25345  itgcn  25362  coe1termlem  25772  coe1term  25773  cxpval  26172  leibpilem2  26446  leibpi  26447  prmorcht  26682  sqff1o  26686  pclogsum  26718  dchr1  26760  dchr2sum  26776  sum2dchr  26777  lgsval  26804  lgsneg  26824  lgsdilem  26827  lgsdir2  26833  lgsdir  26835  dchrisum0flblem2  27012  dchrisum0flb  27013  ostth1  27136  mptprop  31920  fzto1st  32262  psgnfzto1st  32264  sgnsv  32319  sgnsval  32320  elrspunsn  32547  smatfval  32775  1smat1  32784  indval  33011  indfval  33014  prodindf  33021  ddeval1  33232  ddeval0  33233  eulerpartlemgvv  33375  sgnneg  33539  signsvvfval  33589  signsvfn  33593  hashreprin  33632  circlemeth  33652  kur14  34207  ex-sategoelel  34412  mrsubrn  34504  finxpeq1  36267  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem23  36511  poimirlem27  36515  itg2addnclem  36539  itg2gt0cn  36543  ibladdnclem  36544  iblabsnclem  36551  ftc1anclem5  36565  ftc1anc  36569  ftc2nc  36570  metakunt11  40995  metakunt32  41016  frlmvscadiccat  41080  evlsbagval  41138  selvvvval  41157  fsuppind  41162  pw2f1ocnv  41776  flcidc  41916  cantnfresb  42074  refsum2cnlem1  43721  icccncfext  44603  fourierdlem112  44934  fourierswlem  44946  fouriersw  44947  etransclem1  44951  etransclem5  44955  etransclem17  44967  etransclem32  44982  etransclem41  44991  hoidmv1lelem2  45308  ovnhoi  45319  hspdifhsp  45332  hspmbl  45345  hoimbl  45347  ovnsubadd2  45362  suppmptcfin  47055  linc0scn0  47104  linc1  47106  lcoss  47117  el0ldep  47147