Theorem ifbid 4549

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  ifbieq1d  4550  ifbieq2d  4552  ifbieq12d  4554  ifbieq12d2  4560  ifan  4579  ifor  4580  rabsnif  4723  suppsnop  8203  resixpfo  8976  pw2f1olem  9116  unxpdomlem1  9286  cantnflem1d  9728  cantnflem1  9729  ssttrcl  9755  ttrclselem2  9766  dfac12lem1  10184  ttukeylem3  10551  2resupmax  13230  xaddval  13265  xmulcom  13308  xmulneg1  13311  repswswrd  14822  ccatco  14874  sgnval  15127  sumeq1  15725  sumsplit  15804  prodeq1f  15942  prodeq1  15943  rpnnen2lem1  16250  rpnnen2lem2  16251  rpnnen2lem10  16259  sadadd2lem2  16487  sadfval  16489  sadcp1  16492  sadadd2lem  16496  sadcom  16500  pcmpt  16930  pcmpt2  16931  pcfac  16937  prmrec  16960  ramcl  17067  acsfn  17702  setcepi  18133  mgmnsgrpex  18944  sgrpnmndex  18945  frgpup3lem  19795  dpjrid  20082  abvtrivd  20833  obsip  21741  uvcval  21805  uvcvval  21806  psrlidm  21982  psrridm  21983  psrascl  21999  mvrval  22002  mvrval2  22003  mvrf1  22006  mplmonmul  22054  mplcoe1  22055  mplcoe3  22056  mplcoe5  22058  evlslem3  22104  mhpsclcl  22151  psdfval  22162  psdmplcl  22166  psdmul  22170  psdmvr  22173  coe1tm  22276  coe1tmfv2  22278  gsummoncoe1  22312  mat1comp  22446  mamulid  22447  mamurid  22448  mat1ov  22454  mattpos1  22462  mat1dimid  22480  scmateALT  22518  scmatscm  22519  1mavmul  22554  marrepval  22568  marrepeval  22569  marepvval  22573  ma1repveval  22577  1marepvmarrepid  22581  mdetdiagid  22606  mdetunilem8  22625  mdetunilem9  22626  maducoeval  22645  maducoeval2  22646  madutpos  22648  madugsum  22649  minmar1val  22654  minmar1eval  22655  symgmatr01lem  22659  symgmatr01  22660  gsummatr01lem3  22663  gsummatr01lem4  22664  gsummatr01  22665  m2cpm  22747  m2cpminvid2lem  22760  decpmatid  22776  monmatcollpw  22785  mp2pm2mplem4  22815  chmatval  22835  fvmptnn04if  22855  fclsval  24016  tmsxpsval2  24552  dscmet  24585  dscopn  24586  ovolicc1  25551  ovolicc  25558  i1f1lem  25724  itg11  25726  i1fpos  25741  itg2uba  25778  itg2split  25784  itg2monolem1  25785  itg2cnlem1  25796  itg2cnlem2  25797  itg2cn  25798  ibllem  25799  isibl  25800  itgeq1f  25806  itgeq1fOLD  25807  itgeq1  25808  cbvitgv  25812  itgresr  25814  iblpos  25828  itgposval  25831  i1fibl  25843  ibladdlem  25855  iblabslem  25863  itgcn  25880  coe1termlem  26297  coe1term  26298  cxpval  26706  leibpilem2  26984  leibpi  26985  prmorcht  27221  sqff1o  27225  pclogsum  27259  dchr1  27301  dchr2sum  27317  sum2dchr  27318  lgsval  27345  lgsneg  27365  lgsdilem  27368  lgsdir2  27374  lgsdir  27376  dchrisum0flblem2  27553  dchrisum0flb  27554  ostth1  27677  mptprop  32707  indval  32838  indfval  32841  prodindf  32848  fzto1st  33123  psgnfzto1st  33125  sgnsv  33180  sgnsval  33181  elrspunsn  33457  smatfval  33794  1smat1  33803  ddeval1  34235  ddeval0  34236  eulerpartlemgvv  34378  sgnneg  34543  signsvvfval  34593  signsvfn  34597  hashreprin  34635  circlemeth  34655  kur14  35221  ex-sategoelel  35426  mrsubrn  35518  prodeq12sdv  36219  itgeq12sdv  36220  cbvitgvw2  36249  cbvitgdavw  36282  cbvitgdavw2  36298  finxpeq1  37387  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem27  37654  itg2addnclem  37678  itg2gt0cn  37682  ibladdnclem  37683  iblabsnclem  37690  ftc1anclem5  37704  ftc1anc  37708  ftc2nc  37709  metakunt11  42216  metakunt32  42237  frlmvscadiccat  42516  fiabv  42546  evlsbagval  42576  selvvvval  42595  fsuppind  42600  pw2f1ocnv  43049  flcidc  43182  cantnfresb  43337  refsum2cnlem1  45042  icccncfext  45902  fourierdlem112  46233  fourierswlem  46245  fouriersw  46246  etransclem1  46250  etransclem5  46254  etransclem17  46266  etransclem32  46281  etransclem41  46290  hoidmv1lelem2  46607  ovnhoi  46618  hspdifhsp  46631  hspmbl  46644  hoimbl  46646  ovnsubadd2  46661  suppmptcfin  48292  linc0scn0  48340  linc1  48342  lcoss  48353  el0ldep  48383