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 205   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  ifbieq1d  4480  ifbieq2d  4482  ifbieq12d  4484  ifbieq12d2  4490  ifan  4509  ifor  4510  rabsnif  4656  suppsnop  7965  resixpfo  8682  pw2f1olem  8816  unxpdomlem1  8956  cantnflem1d  9376  cantnflem1  9377  dfac12lem1  9830  ttukeylem3  10198  2resupmax  12851  xaddval  12886  xmulcom  12929  xmulneg1  12932  repswswrd  14425  ccatco  14476  sgnval  14727  sumeq1  15328  sumsplit  15408  prodeq1f  15546  rpnnen2lem1  15851  rpnnen2lem2  15852  rpnnen2lem10  15860  sadadd2lem2  16085  sadfval  16087  sadcp1  16090  sadadd2lem  16094  sadcom  16098  pcmpt  16521  pcmpt2  16522  pcfac  16528  prmrec  16551  ramcl  16658  acsfn  17285  setcepi  17719  mgmnsgrpex  18485  sgrpnmndex  18486  frgpup3lem  19298  dpjrid  19580  abvtrivd  20015  obsip  20838  uvcval  20902  uvcvval  20903  psrlidm  21082  psrridm  21083  mvrval  21100  mvrval2  21101  mvrf1  21104  mplmonmul  21147  mplcoe1  21148  mplcoe3  21149  mplcoe5  21151  evlslem3  21200  mhpsclcl  21247  coe1tm  21354  coe1tmfv2  21356  gsummoncoe1  21385  mat1comp  21497  mamulid  21498  mamurid  21499  mat1ov  21505  mattpos1  21513  mat1dimid  21531  scmateALT  21569  scmatscm  21570  1mavmul  21605  marrepval  21619  marrepeval  21620  marepvval  21624  ma1repveval  21628  1marepvmarrepid  21632  mdetdiagid  21657  mdetunilem8  21676  mdetunilem9  21677  maducoeval  21696  maducoeval2  21697  madutpos  21699  madugsum  21700  minmar1val  21705  minmar1eval  21706  symgmatr01lem  21710  symgmatr01  21711  gsummatr01lem3  21714  gsummatr01lem4  21715  gsummatr01  21716  m2cpm  21798  m2cpminvid2lem  21811  decpmatid  21827  monmatcollpw  21836  mp2pm2mplem4  21866  chmatval  21886  fvmptnn04if  21906  fclsval  23067  tmsxpsval2  23601  dscmet  23634  dscopn  23635  ovolicc1  24585  ovolicc  24592  i1f1lem  24758  itg11  24760  i1fpos  24776  itg2uba  24813  itg2split  24819  itg2monolem1  24820  itg2cnlem1  24831  itg2cnlem2  24832  itg2cn  24833  ibllem  24834  isibl  24835  itgeq1f  24841  itgresr  24848  iblpos  24862  itgposval  24865  i1fibl  24877  ibladdlem  24889  iblabslem  24897  itgcn  24914  coe1termlem  25324  coe1term  25325  cxpval  25724  leibpilem2  25996  leibpi  25997  prmorcht  26232  sqff1o  26236  pclogsum  26268  dchr1  26310  dchr2sum  26326  sum2dchr  26327  lgsval  26354  lgsneg  26374  lgsdilem  26377  lgsdir2  26383  lgsdir  26385  dchrisum0flblem2  26562  dchrisum0flb  26563  ostth1  26686  mptprop  30933  fzto1st  31272  psgnfzto1st  31274  sgnsv  31329  sgnsval  31330  smatfval  31647  1smat1  31656  indval  31881  indfval  31884  prodindf  31891  ddeval1  32102  ddeval0  32103  eulerpartlemgvv  32243  sgnneg  32407  signsvvfval  32457  signsvfn  32461  hashreprin  32500  circlemeth  32520  kur14  33078  ex-sategoelel  33283  mrsubrn  33375  ssttrcl  33701  ttrclselem2  33712  finxpeq1  35484  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem22  35726  poimirlem23  35727  poimirlem27  35731  itg2addnclem  35755  itg2gt0cn  35759  ibladdnclem  35760  iblabsnclem  35767  ftc1anclem5  35781  ftc1anc  35785  ftc2nc  35786  metakunt11  40063  metakunt32  40084  frlmvscadiccat  40163  evlsbagval  40198  fsuppind  40202  mhphf  40208  pw2f1ocnv  40775  flcidc  40915  refsum2cnlem1  42469  icccncfext  43318  fourierdlem112  43649  fourierswlem  43661  fouriersw  43662  etransclem1  43666  etransclem5  43670  etransclem17  43682  etransclem32  43697  etransclem41  43706  hoidmv1lelem2  44020  ovnhoi  44031  hspdifhsp  44044  hspmbl  44057  hoimbl  44059  ovnsubadd2  44074  suppmptcfin  45603  linc0scn0  45652  linc1  45654  lcoss  45665  el0ldep  45695