Theorem ifbid 4505

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  ifbieq1d  4506  ifbieq2d  4508  ifbieq12d  4510  ifbieq12d2  4516  ifan  4535  ifor  4536  rabsnif  4682  suppsnop  8130  resixpfo  8886  pw2f1olem  9021  unxpdomlem1  9168  cantnflem1d  9609  cantnflem1  9610  ssttrcl  9636  ttrclselem2  9647  dfac12lem1  10066  ttukeylem3  10433  2resupmax  13115  xaddval  13150  xmulcom  13193  xmulneg1  13196  repswswrd  14719  ccatco  14770  sgnval  15023  sumeq1  15624  sumsplit  15703  prodeq1f  15841  prodeq1  15842  rpnnen2lem1  16151  rpnnen2lem2  16152  rpnnen2lem10  16160  sadadd2lem2  16389  sadfval  16391  sadcp1  16394  sadadd2lem  16398  sadcom  16402  pcmpt  16832  pcmpt2  16833  pcfac  16839  prmrec  16862  ramcl  16969  acsfn  17594  setcepi  18024  mgmnsgrpex  18871  sgrpnmndex  18872  frgpup3lem  19721  dpjrid  20008  abvtrivd  20780  obsip  21691  uvcval  21755  uvcvval  21756  psrlidm  21932  psrridm  21933  psrascl  21949  mvrval  21952  mvrval2  21953  mvrf1  21956  mplmonmul  22006  mplcoe1  22007  mplcoe3  22008  mplcoe5  22010  evlslem3  22050  mhpsclcl  22105  psdfval  22116  psdmplcl  22120  psdmul  22124  psdmvr  22127  coe1tm  22230  coe1tmfv2  22232  gsummoncoe1  22267  mat1comp  22399  mamulid  22400  mamurid  22401  mat1ov  22407  mattpos1  22415  mat1dimid  22433  scmateALT  22471  scmatscm  22472  1mavmul  22507  marrepval  22521  marrepeval  22522  marepvval  22526  ma1repveval  22530  1marepvmarrepid  22534  mdetdiagid  22559  mdetunilem8  22578  mdetunilem9  22579  maducoeval  22598  maducoeval2  22599  madutpos  22601  madugsum  22602  minmar1val  22607  minmar1eval  22608  symgmatr01lem  22612  symgmatr01  22613  gsummatr01lem3  22616  gsummatr01lem4  22617  gsummatr01  22618  m2cpm  22700  m2cpminvid2lem  22713  decpmatid  22729  monmatcollpw  22738  mp2pm2mplem4  22768  chmatval  22788  fvmptnn04if  22808  fclsval  23967  tmsxpsval2  24498  dscmet  24531  dscopn  24532  ovolicc1  25488  ovolicc  25495  i1f1lem  25661  itg11  25663  i1fpos  25678  itg2uba  25715  itg2split  25721  itg2monolem1  25722  itg2cnlem1  25733  itg2cnlem2  25734  itg2cn  25735  ibllem  25736  isibl  25737  itgeq1f  25743  itgeq1fOLD  25744  itgeq1  25745  cbvitgv  25749  itgresr  25751  iblpos  25765  itgposval  25768  i1fibl  25780  ibladdlem  25792  iblabslem  25800  itgcn  25817  coe1termlem  26234  coe1term  26235  cxpval  26644  leibpilem2  26922  leibpi  26923  prmorcht  27159  sqff1o  27163  pclogsum  27197  dchr1  27239  dchr2sum  27255  sum2dchr  27256  lgsval  27283  lgsneg  27303  lgsdilem  27306  lgsdir2  27312  lgsdir  27314  dchrisum0flblem2  27491  dchrisum0flb  27492  ostth1  27615  partfun2  32770  mptprop  32792  sgnneg  32929  indval  32947  indfval  32950  prodindf  32959  indsn  32960  fzto1st  33201  psgnfzto1st  33203  sgnsv  33258  sgnsval  33259  elrspunsn  33526  mvrvalind  33719  mplvrpmrhm  33728  psrmonmul  33731  psrmonmul2  33732  psrmonprod  33733  mplmonprod  33735  esplysply  33752  esplyfval1  33754  esplyfvaln  33755  esplyind  33756  smatfval  33977  1smat1  33986  ddeval1  34416  ddeval0  34417  eulerpartlemgvv  34558  signsvvfval  34760  signsvfn  34764  hashreprin  34802  circlemeth  34822  kur14  35436  ex-sategoelel  35641  mrsubrn  35733  prodeq12sdv  36438  itgeq12sdv  36439  cbvitgvw2  36468  cbvitgdavw  36501  cbvitgdavw2  36517  finxpeq1  37645  poimirlem5  37880  poimirlem6  37881  poimirlem7  37882  poimirlem8  37883  poimirlem10  37885  poimirlem11  37886  poimirlem12  37887  poimirlem15  37890  poimirlem16  37891  poimirlem17  37892  poimirlem18  37893  poimirlem19  37894  poimirlem20  37895  poimirlem21  37896  poimirlem22  37897  poimirlem23  37898  poimirlem27  37902  itg2addnclem  37926  itg2gt0cn  37930  ibladdnclem  37931  iblabsnclem  37938  ftc1anclem5  37952  ftc1anc  37956  ftc2nc  37957  frlmvscadiccat  42880  fiabv  42910  evlsbagval  42931  selvvvval  42947  fsuppind  42952  pw2f1ocnv  43398  flcidc  43531  cantnfresb  43685  refsum2cnlem1  45401  icccncfext  46249  fourierdlem112  46580  fourierswlem  46592  fouriersw  46593  etransclem1  46597  etransclem5  46601  etransclem17  46613  etransclem32  46628  etransclem41  46637  hoidmv1lelem2  46954  ovnhoi  46965  hspdifhsp  46978  hspmbl  46991  hoimbl  46993  ovnsubadd2  47008  suppmptcfin  48740  linc0scn0  48787  linc1  48789  lcoss  48800  el0ldep  48830