Theorem ifbid 4487

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4465

This theorem is referenced by:  ifbieq1d  4488  ifbieq2d  4490  ifbieq12d  4492  ifbieq12d2  4498  ifan  4517  ifor  4518  rabsnif  4664  suppsnop  7978  resixpfo  8698  pw2f1olem  8832  unxpdomlem1  8988  cantnflem1d  9407  cantnflem1  9408  ssttrcl  9434  ttrclselem2  9445  dfac12lem1  9883  ttukeylem3  10251  2resupmax  12904  xaddval  12939  xmulcom  12982  xmulneg1  12985  repswswrd  14478  ccatco  14529  sgnval  14780  sumeq1  15381  sumsplit  15461  prodeq1f  15599  rpnnen2lem1  15904  rpnnen2lem2  15905  rpnnen2lem10  15913  sadadd2lem2  16138  sadfval  16140  sadcp1  16143  sadadd2lem  16147  sadcom  16151  pcmpt  16574  pcmpt2  16575  pcfac  16581  prmrec  16604  ramcl  16711  acsfn  17349  setcepi  17784  mgmnsgrpex  18551  sgrpnmndex  18552  frgpup3lem  19364  dpjrid  19646  abvtrivd  20081  obsip  20909  uvcval  20973  uvcvval  20974  psrlidm  21153  psrridm  21154  mvrval  21171  mvrval2  21172  mvrf1  21175  mplmonmul  21218  mplcoe1  21219  mplcoe3  21220  mplcoe5  21222  evlslem3  21271  mhpsclcl  21318  coe1tm  21425  coe1tmfv2  21427  gsummoncoe1  21456  mat1comp  21570  mamulid  21571  mamurid  21572  mat1ov  21578  mattpos1  21586  mat1dimid  21604  scmateALT  21642  scmatscm  21643  1mavmul  21678  marrepval  21692  marrepeval  21693  marepvval  21697  ma1repveval  21701  1marepvmarrepid  21705  mdetdiagid  21730  mdetunilem8  21749  mdetunilem9  21750  maducoeval  21769  maducoeval2  21770  madutpos  21772  madugsum  21773  minmar1val  21778  minmar1eval  21779  symgmatr01lem  21783  symgmatr01  21784  gsummatr01lem3  21787  gsummatr01lem4  21788  gsummatr01  21789  m2cpm  21871  m2cpminvid2lem  21884  decpmatid  21900  monmatcollpw  21909  mp2pm2mplem4  21939  chmatval  21959  fvmptnn04if  21979  fclsval  23140  tmsxpsval2  23676  dscmet  23709  dscopn  23710  ovolicc1  24661  ovolicc  24668  i1f1lem  24834  itg11  24836  i1fpos  24852  itg2uba  24889  itg2split  24895  itg2monolem1  24896  itg2cnlem1  24907  itg2cnlem2  24908  itg2cn  24909  ibllem  24910  isibl  24911  itgeq1f  24917  itgresr  24924  iblpos  24938  itgposval  24941  i1fibl  24953  ibladdlem  24965  iblabslem  24973  itgcn  24990  coe1termlem  25400  coe1term  25401  cxpval  25800  leibpilem2  26072  leibpi  26073  prmorcht  26308  sqff1o  26312  pclogsum  26344  dchr1  26386  dchr2sum  26402  sum2dchr  26403  lgsval  26430  lgsneg  26450  lgsdilem  26453  lgsdir2  26459  lgsdir  26461  dchrisum0flblem2  26638  dchrisum0flb  26639  ostth1  26762  mptprop  31010  fzto1st  31349  psgnfzto1st  31351  sgnsv  31406  sgnsval  31407  smatfval  31724  1smat1  31733  indval  31960  indfval  31963  prodindf  31970  ddeval1  32181  ddeval0  32182  eulerpartlemgvv  32322  sgnneg  32486  signsvvfval  32536  signsvfn  32540  hashreprin  32579  circlemeth  32599  kur14  33157  ex-sategoelel  33362  mrsubrn  33454  finxpeq1  35536  poimirlem5  35761  poimirlem6  35762  poimirlem7  35763  poimirlem8  35764  poimirlem10  35766  poimirlem11  35767  poimirlem12  35768  poimirlem15  35771  poimirlem16  35772  poimirlem17  35773  poimirlem18  35774  poimirlem19  35775  poimirlem20  35776  poimirlem21  35777  poimirlem22  35778  poimirlem23  35779  poimirlem27  35783  itg2addnclem  35807  itg2gt0cn  35811  ibladdnclem  35812  iblabsnclem  35819  ftc1anclem5  35833  ftc1anc  35837  ftc2nc  35838  metakunt11  40115  metakunt32  40136  frlmvscadiccat  40217  evlsbagval  40255  fsuppind  40259  mhphf  40265  pw2f1ocnv  40839  flcidc  40979  refsum2cnlem1  42533  icccncfext  43382  fourierdlem112  43713  fourierswlem  43725  fouriersw  43726  etransclem1  43730  etransclem5  43734  etransclem17  43746  etransclem32  43761  etransclem41  43770  hoidmv1lelem2  44084  ovnhoi  44095  hspdifhsp  44108  hspmbl  44121  hoimbl  44123  ovnsubadd2  44138  suppmptcfin  45667  linc0scn0  45716  linc1  45718  lcoss  45729  el0ldep  45759