Theorem ifbid 4514

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ifcif 4491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-if 4492

This theorem is referenced by:  ifbieq1d  4515  ifbieq2d  4517  ifbieq12d  4519  ifbieq12d2  4525  ifan  4544  ifor  4545  rabsnif  4689  suppsnop  8114  resixpfo  8881  pw2f1olem  9027  unxpdomlem1  9201  cantnflem1d  9633  cantnflem1  9634  ssttrcl  9660  ttrclselem2  9671  dfac12lem1  10088  ttukeylem3  10456  2resupmax  13117  xaddval  13152  xmulcom  13195  xmulneg1  13198  repswswrd  14684  ccatco  14736  sgnval  14985  sumeq1  15585  sumsplit  15664  prodeq1f  15802  rpnnen2lem1  16107  rpnnen2lem2  16108  rpnnen2lem10  16116  sadadd2lem2  16341  sadfval  16343  sadcp1  16346  sadadd2lem  16350  sadcom  16354  pcmpt  16775  pcmpt2  16776  pcfac  16782  prmrec  16805  ramcl  16912  acsfn  17553  setcepi  17988  mgmnsgrpex  18755  sgrpnmndex  18756  frgpup3lem  19573  dpjrid  19855  abvtrivd  20355  obsip  21164  uvcval  21228  uvcvval  21229  psrlidm  21409  psrridm  21410  mvrval  21427  mvrval2  21428  mvrf1  21431  mplmonmul  21474  mplcoe1  21475  mplcoe3  21476  mplcoe5  21478  evlslem3  21527  mhpsclcl  21574  coe1tm  21681  coe1tmfv2  21683  gsummoncoe1  21712  mat1comp  21826  mamulid  21827  mamurid  21828  mat1ov  21834  mattpos1  21842  mat1dimid  21860  scmateALT  21898  scmatscm  21899  1mavmul  21934  marrepval  21948  marrepeval  21949  marepvval  21953  ma1repveval  21957  1marepvmarrepid  21961  mdetdiagid  21986  mdetunilem8  22005  mdetunilem9  22006  maducoeval  22025  maducoeval2  22026  madutpos  22028  madugsum  22029  minmar1val  22034  minmar1eval  22035  symgmatr01lem  22039  symgmatr01  22040  gsummatr01lem3  22043  gsummatr01lem4  22044  gsummatr01  22045  m2cpm  22127  m2cpminvid2lem  22140  decpmatid  22156  monmatcollpw  22165  mp2pm2mplem4  22195  chmatval  22215  fvmptnn04if  22235  fclsval  23396  tmsxpsval2  23932  dscmet  23965  dscopn  23966  ovolicc1  24917  ovolicc  24924  i1f1lem  25090  itg11  25092  i1fpos  25108  itg2uba  25145  itg2split  25151  itg2monolem1  25152  itg2cnlem1  25163  itg2cnlem2  25164  itg2cn  25165  ibllem  25166  isibl  25167  itgeq1f  25173  itgresr  25180  iblpos  25194  itgposval  25197  i1fibl  25209  ibladdlem  25221  iblabslem  25229  itgcn  25246  coe1termlem  25656  coe1term  25657  cxpval  26056  leibpilem2  26328  leibpi  26329  prmorcht  26564  sqff1o  26568  pclogsum  26600  dchr1  26642  dchr2sum  26658  sum2dchr  26659  lgsval  26686  lgsneg  26706  lgsdilem  26709  lgsdir2  26715  lgsdir  26717  dchrisum0flblem2  26894  dchrisum0flb  26895  ostth1  27018  mptprop  31680  fzto1st  32022  psgnfzto1st  32024  sgnsv  32079  sgnsval  32080  smatfval  32465  1smat1  32474  indval  32701  indfval  32704  prodindf  32711  ddeval1  32922  ddeval0  32923  eulerpartlemgvv  33065  sgnneg  33229  signsvvfval  33279  signsvfn  33283  hashreprin  33322  circlemeth  33342  kur14  33897  ex-sategoelel  34102  mrsubrn  34194  finxpeq1  35930  poimirlem5  36156  poimirlem6  36157  poimirlem7  36158  poimirlem8  36159  poimirlem10  36161  poimirlem11  36162  poimirlem12  36163  poimirlem15  36166  poimirlem16  36167  poimirlem17  36168  poimirlem18  36169  poimirlem19  36170  poimirlem20  36171  poimirlem21  36172  poimirlem22  36173  poimirlem23  36174  poimirlem27  36178  itg2addnclem  36202  itg2gt0cn  36206  ibladdnclem  36207  iblabsnclem  36214  ftc1anclem5  36228  ftc1anc  36232  ftc2nc  36233  metakunt11  40660  metakunt32  40681  frlmvscadiccat  40749  evlsbagval  40806  fsuppind  40823  mhphf  40829  pw2f1ocnv  41419  flcidc  41559  cantnfresb  41717  refsum2cnlem1  43364  icccncfext  44248  fourierdlem112  44579  fourierswlem  44591  fouriersw  44592  etransclem1  44596  etransclem5  44600  etransclem17  44612  etransclem32  44627  etransclem41  44636  hoidmv1lelem2  44953  ovnhoi  44964  hspdifhsp  44977  hspmbl  44990  hoimbl  44992  ovnsubadd2  45007  suppmptcfin  46575  linc0scn0  46624  linc1  46626  lcoss  46637  el0ldep  46667