Theorem ifbid 4571

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  ifbieq1d  4572  ifbieq2d  4574  ifbieq12d  4576  ifbieq12d2  4582  ifan  4601  ifor  4602  rabsnif  4748  suppsnop  8219  resixpfo  8994  pw2f1olem  9142  unxpdomlem1  9313  cantnflem1d  9757  cantnflem1  9758  ssttrcl  9784  ttrclselem2  9795  dfac12lem1  10213  ttukeylem3  10580  2resupmax  13250  xaddval  13285  xmulcom  13328  xmulneg1  13331  repswswrd  14832  ccatco  14884  sgnval  15137  sumeq1  15737  sumsplit  15816  prodeq1f  15954  prodeq1  15955  rpnnen2lem1  16262  rpnnen2lem2  16263  rpnnen2lem10  16271  sadadd2lem2  16496  sadfval  16498  sadcp1  16501  sadadd2lem  16505  sadcom  16509  pcmpt  16939  pcmpt2  16940  pcfac  16946  prmrec  16969  ramcl  17076  acsfn  17717  setcepi  18155  mgmnsgrpex  18966  sgrpnmndex  18967  frgpup3lem  19819  dpjrid  20106  abvtrivd  20855  obsip  21764  uvcval  21828  uvcvval  21829  psrlidm  22005  psrridm  22006  psrascl  22022  mvrval  22025  mvrval2  22026  mvrf1  22029  mplmonmul  22077  mplcoe1  22078  mplcoe3  22079  mplcoe5  22081  evlslem3  22127  mhpsclcl  22174  psdfval  22185  psdmplcl  22189  psdmul  22193  coe1tm  22297  coe1tmfv2  22299  gsummoncoe1  22333  mat1comp  22467  mamulid  22468  mamurid  22469  mat1ov  22475  mattpos1  22483  mat1dimid  22501  scmateALT  22539  scmatscm  22540  1mavmul  22575  marrepval  22589  marrepeval  22590  marepvval  22594  ma1repveval  22598  1marepvmarrepid  22602  mdetdiagid  22627  mdetunilem8  22646  mdetunilem9  22647  maducoeval  22666  maducoeval2  22667  madutpos  22669  madugsum  22670  minmar1val  22675  minmar1eval  22676  symgmatr01lem  22680  symgmatr01  22681  gsummatr01lem3  22684  gsummatr01lem4  22685  gsummatr01  22686  m2cpm  22768  m2cpminvid2lem  22781  decpmatid  22797  monmatcollpw  22806  mp2pm2mplem4  22836  chmatval  22856  fvmptnn04if  22876  fclsval  24037  tmsxpsval2  24573  dscmet  24606  dscopn  24607  ovolicc1  25570  ovolicc  25577  i1f1lem  25743  itg11  25745  i1fpos  25761  itg2uba  25798  itg2split  25804  itg2monolem1  25805  itg2cnlem1  25816  itg2cnlem2  25817  itg2cn  25818  ibllem  25819  isibl  25820  itgeq1f  25826  itgeq1fOLD  25827  itgeq1  25828  cbvitgv  25832  itgresr  25834  iblpos  25848  itgposval  25851  i1fibl  25863  ibladdlem  25875  iblabslem  25883  itgcn  25900  coe1termlem  26317  coe1term  26318  cxpval  26724  leibpilem2  27002  leibpi  27003  prmorcht  27239  sqff1o  27243  pclogsum  27277  dchr1  27319  dchr2sum  27335  sum2dchr  27336  lgsval  27363  lgsneg  27383  lgsdilem  27386  lgsdir2  27392  lgsdir  27394  dchrisum0flblem2  27571  dchrisum0flb  27572  ostth1  27695  mptprop  32710  fzto1st  33096  psgnfzto1st  33098  sgnsv  33153  sgnsval  33154  elrspunsn  33422  smatfval  33741  1smat1  33750  indval  33977  indfval  33980  prodindf  33987  ddeval1  34198  ddeval0  34199  eulerpartlemgvv  34341  sgnneg  34505  signsvvfval  34555  signsvfn  34559  hashreprin  34597  circlemeth  34617  kur14  35184  ex-sategoelel  35389  mrsubrn  35481  prodeq12sdv  36184  itgeq12sdv  36185  cbvitgvw2  36214  cbvitgdavw  36247  cbvitgdavw2  36263  finxpeq1  37352  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem27  37607  itg2addnclem  37631  itg2gt0cn  37635  ibladdnclem  37636  iblabsnclem  37643  ftc1anclem5  37657  ftc1anc  37661  ftc2nc  37662  metakunt11  42172  metakunt32  42193  frlmvscadiccat  42461  fiabv  42491  evlsbagval  42521  selvvvval  42540  fsuppind  42545  pw2f1ocnv  42994  flcidc  43131  cantnfresb  43286  refsum2cnlem1  44937  icccncfext  45808  fourierdlem112  46139  fourierswlem  46151  fouriersw  46152  etransclem1  46156  etransclem5  46160  etransclem17  46172  etransclem32  46187  etransclem41  46196  hoidmv1lelem2  46513  ovnhoi  46524  hspdifhsp  46537  hspmbl  46550  hoimbl  46552  ovnsubadd2  46567  suppmptcfin  48104  linc0scn0  48152  linc1  48154  lcoss  48165  el0ldep  48195