Theorem ifbid 4508

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  ifcif 4484

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4485

This theorem is used by:  ifbieq1d  4509  ifbieq2d  4511  ifbieq12d  4513  ifbieq12d2  4519  ifan  4538  ifor  4539  rabsnif  4683  suppsnop  8206  resixpfo  8975  pw2f1olem  9111  unxpdomlem1  9258  cantnflem1d  9699  cantnflem1  9700  ssttrcl  9726  ttrclselem2  9737  dfac12lem1  10232  ttukeylem3  10599  indval  12333  indfval  12337  2resupmax  13328  xaddval  13363  xmulcom  13406  xmulneg1  13409  repswswrd  14946  ccatco  14997  sgnval  15253  sgnneg  15265  sumeq1  15868  sumsplit  15946  prodeq1f  16087  prodeq1  16088  rpnnen2lem1  16394  rpnnen2lem2  16395  rpnnen2lem10  16403  sadadd2lem2  16632  sadfval  16634  sadcp1  16637  sadadd2lem  16641  sadcom  16645  pcmpt  17082  pcmpt2  17083  pcfac  17089  prmrec  17112  ramcl  17219  acsfn  17845  setcepi  18275  mgmnsgrpex  19142  sgrpnmndex  19143  frgpup3lem  20003  dpjrid  20290  abvtrivd  21101  obsip  22039  uvcval  22103  uvcvval  22104  psrlidm  22281  psrridm  22282  psrascl  22298  mvrval  22301  mvrval2  22302  mvrf1  22305  mplmonmul  22357  mplcoe1  22358  mplcoe3  22359  mplcoe5  22361  evlslem3  22401  selvvvval  22463  mhpsclcl  22480  psdfval  22491  psdmplcl  22495  psdmul  22499  psdmvr  22502  coe1tm  22604  coe1tmfv2  22606  gsummoncoe1  22638  mat1comp  22767  mamulid  22768  mamurid  22769  mat1ov  22775  mattpos1  22783  mat1dimid  22801  scmateALT  22839  scmatscm  22840  1mavmul  22875  marrepval  22889  marrepeval  22890  marepvval  22894  ma1repveval  22898  1marepvmarrepid  22902  mdetdiagid  22927  mdetunilem8  22946  mdetunilem9  22947  maducoeval  22966  maducoeval2  22967  madutpos  22969  madugsum  22970  minmar1val  22975  minmar1eval  22976  symgmatr01lem  22980  symgmatr01  22981  gsummatr01lem3  22984  gsummatr01lem4  22985  gsummatr01  22986  m2cpm  23071  m2cpminvid2lem  23084  decpmatid  23100  monmatcollpw  23109  mp2pm2mplem4  23139  chmatval  23159  fvmptnn04if  23179  fclsval  24339  tmsxpsval2  24870  dscmet  24903  dscopn  24904  ovolicc1  25849  ovolicc  25856  i1f1lem  26022  itg11  26024  i1fpos  26039  itg2uba  26076  itg2split  26082  itg2monolem1  26083  itg2cnlem1  26094  itg2cnlem2  26095  itg2cn  26096  ibllem  26097  isibl  26098  itgeq1f  26104  itgeq1  26105  cbvitgv  26109  itgresr  26111  iblpos  26125  itgposval  26128  i1fibl  26140  ibladdlem  26152  iblabslem  26160  itgcn  26177  coe1termlem  26589  coe1term  26590  cxpval  27004  leibpilem2  27281  leibpi  27282  prmorcht  27517  sqff1o  27521  pclogsum  27554  dchr1  27596  dchr2sum  27612  sum2dchr  27613  lgsval  27640  lgsneg  27660  lgsdilem  27663  lgsdir2  27669  lgsdir  27671  dchrisum0flblem2  27848  dchrisum0flb  27849  ostth1  27972  partfun2  33324  mptprop  33345  prodindf  33482  indsn  33483  fzto1st  33717  psgnfzto1st  33719  sgnsv  33774  sgnsval  33775  elrspunsn  34032  mvrvalind  34223  mplvrpmrhm  34232  psrmonmul  34235  psrmonmul2  34236  psrmonprod  34237  mplmonprod  34239  esplysply  34256  esplyfval1  34258  esplyfvaln  34259  esplyind  34260  smatfval  34480  1smat1  34489  ddeval1  34920  ddeval0  34921  eulerpartlemgvv  35061  signsvvfval  35260  signsvfn  35264  hashreprin  35302  circlemeth  35322  kur14  36102  ex-sategoelel  36307  mrsubrn  36399  prodeq12sdv  37134  itgeq12sdv  37135  cbvitgvw2  37164  cbvitgdavw  37197  cbvitgdavw2  37213  finxpeq1  38449  poimirlem5  38683  poimirlem6  38684  poimirlem7  38685  poimirlem8  38686  poimirlem10  38688  poimirlem11  38689  poimirlem12  38690  poimirlem15  38693  poimirlem16  38694  poimirlem17  38695  poimirlem18  38696  poimirlem19  38697  poimirlem20  38698  poimirlem21  38699  poimirlem22  38700  poimirlem23  38701  poimirlem27  38705  itg2addnclem  38729  itg2gt0cn  38733  ibladdnclem  38734  iblabsnclem  38741  ftc1anclem5  38755  ftc1anc  38759  ftc2nc  38760  frlmvscadiccat  43713  fiabv  43740  evlsbagval  43754  fsuppind  43758  pw2f1ocnv  44184  flcidc  44312  cantnfresb  44466  refsum2cnlem1  46193  icccncfext  47036  fourierdlem112  47367  fourierswlem  47379  fouriersw  47380  etransclem1  47384  etransclem5  47388  etransclem17  47400  etransclem32  47415  etransclem41  47424  hoidmv1lelem2  47741  ovnhoi  47752  hspdifhsp  47765  hspmbl  47778  hoimbl  47780  ovnsubadd2  47795  suppmptcfin  49627  linc0scn0  49674  linc1  49676  lcoss  49687  el0ldep  49717  parhomval  50882  parhomvaln0  50892  parswapval  50915