Theorem ifbid 4553

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-if 4531

This theorem is referenced by:  ifbieq1d  4554  ifbieq2d  4556  ifbieq12d  4558  ifbieq12d2  4564  ifan  4583  ifor  4584  rabsnif  4727  suppsnop  8201  resixpfo  8974  pw2f1olem  9114  unxpdomlem1  9283  cantnflem1d  9725  cantnflem1  9726  ssttrcl  9752  ttrclselem2  9763  dfac12lem1  10181  ttukeylem3  10548  2resupmax  13226  xaddval  13261  xmulcom  13304  xmulneg1  13307  repswswrd  14818  ccatco  14870  sgnval  15123  sumeq1  15721  sumsplit  15800  prodeq1f  15938  prodeq1  15939  rpnnen2lem1  16246  rpnnen2lem2  16247  rpnnen2lem10  16255  sadadd2lem2  16483  sadfval  16485  sadcp1  16488  sadadd2lem  16492  sadcom  16496  pcmpt  16925  pcmpt2  16926  pcfac  16932  prmrec  16955  ramcl  17062  acsfn  17703  setcepi  18141  mgmnsgrpex  18956  sgrpnmndex  18957  frgpup3lem  19809  dpjrid  20096  abvtrivd  20849  obsip  21758  uvcval  21822  uvcvval  21823  psrlidm  21999  psrridm  22000  psrascl  22016  mvrval  22019  mvrval2  22020  mvrf1  22023  mplmonmul  22071  mplcoe1  22072  mplcoe3  22073  mplcoe5  22075  evlslem3  22121  mhpsclcl  22168  psdfval  22179  psdmplcl  22183  psdmul  22187  coe1tm  22291  coe1tmfv2  22293  gsummoncoe1  22327  mat1comp  22461  mamulid  22462  mamurid  22463  mat1ov  22469  mattpos1  22477  mat1dimid  22495  scmateALT  22533  scmatscm  22534  1mavmul  22569  marrepval  22583  marrepeval  22584  marepvval  22588  ma1repveval  22592  1marepvmarrepid  22596  mdetdiagid  22621  mdetunilem8  22640  mdetunilem9  22641  maducoeval  22660  maducoeval2  22661  madutpos  22663  madugsum  22664  minmar1val  22669  minmar1eval  22670  symgmatr01lem  22674  symgmatr01  22675  gsummatr01lem3  22678  gsummatr01lem4  22679  gsummatr01  22680  m2cpm  22762  m2cpminvid2lem  22775  decpmatid  22791  monmatcollpw  22800  mp2pm2mplem4  22830  chmatval  22850  fvmptnn04if  22870  fclsval  24031  tmsxpsval2  24567  dscmet  24600  dscopn  24601  ovolicc1  25564  ovolicc  25571  i1f1lem  25737  itg11  25739  i1fpos  25755  itg2uba  25792  itg2split  25798  itg2monolem1  25799  itg2cnlem1  25810  itg2cnlem2  25811  itg2cn  25812  ibllem  25813  isibl  25814  itgeq1f  25820  itgeq1fOLD  25821  itgeq1  25822  cbvitgv  25826  itgresr  25828  iblpos  25842  itgposval  25845  i1fibl  25857  ibladdlem  25869  iblabslem  25877  itgcn  25894  coe1termlem  26311  coe1term  26312  cxpval  26720  leibpilem2  26998  leibpi  26999  prmorcht  27235  sqff1o  27239  pclogsum  27273  dchr1  27315  dchr2sum  27331  sum2dchr  27332  lgsval  27359  lgsneg  27379  lgsdilem  27382  lgsdir2  27388  lgsdir  27390  dchrisum0flblem2  27567  dchrisum0flb  27568  ostth1  27691  mptprop  32712  fzto1st  33105  psgnfzto1st  33107  sgnsv  33162  sgnsval  33163  elrspunsn  33436  smatfval  33755  1smat1  33764  indval  33993  indfval  33996  prodindf  34003  ddeval1  34214  ddeval0  34215  eulerpartlemgvv  34357  sgnneg  34521  signsvvfval  34571  signsvfn  34575  hashreprin  34613  circlemeth  34633  kur14  35200  ex-sategoelel  35405  mrsubrn  35497  prodeq12sdv  36200  itgeq12sdv  36201  cbvitgvw2  36230  cbvitgdavw  36263  cbvitgdavw2  36279  finxpeq1  37368  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem27  37633  itg2addnclem  37657  itg2gt0cn  37661  ibladdnclem  37662  iblabsnclem  37669  ftc1anclem5  37683  ftc1anc  37687  ftc2nc  37688  metakunt11  42196  metakunt32  42217  frlmvscadiccat  42492  fiabv  42522  evlsbagval  42552  selvvvval  42571  fsuppind  42576  pw2f1ocnv  43025  flcidc  43158  cantnfresb  43313  refsum2cnlem1  44974  icccncfext  45842  fourierdlem112  46173  fourierswlem  46185  fouriersw  46186  etransclem1  46190  etransclem5  46194  etransclem17  46206  etransclem32  46221  etransclem41  46230  hoidmv1lelem2  46547  ovnhoi  46558  hspdifhsp  46571  hspmbl  46584  hoimbl  46586  ovnsubadd2  46601  suppmptcfin  48220  linc0scn0  48268  linc1  48270  lcoss  48281  el0ldep  48311