Theorem ifbid 4501

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-if 4478

This theorem is referenced by:  ifbieq1d  4502  ifbieq2d  4504  ifbieq12d  4506  ifbieq12d2  4512  ifan  4531  ifor  4532  rabsnif  4678  suppsnop  8118  resixpfo  8872  pw2f1olem  9007  unxpdomlem1  9154  cantnflem1d  9595  cantnflem1  9596  ssttrcl  9622  ttrclselem2  9633  dfac12lem1  10052  ttukeylem3  10419  2resupmax  13101  xaddval  13136  xmulcom  13179  xmulneg1  13182  repswswrd  14705  ccatco  14756  sgnval  15009  sumeq1  15610  sumsplit  15689  prodeq1f  15827  prodeq1  15828  rpnnen2lem1  16137  rpnnen2lem2  16138  rpnnen2lem10  16146  sadadd2lem2  16375  sadfval  16377  sadcp1  16380  sadadd2lem  16384  sadcom  16388  pcmpt  16818  pcmpt2  16819  pcfac  16825  prmrec  16848  ramcl  16955  acsfn  17580  setcepi  18010  mgmnsgrpex  18854  sgrpnmndex  18855  frgpup3lem  19704  dpjrid  19991  abvtrivd  20763  obsip  21674  uvcval  21738  uvcvval  21739  psrlidm  21915  psrridm  21916  psrascl  21932  mvrval  21935  mvrval2  21936  mvrf1  21939  mplmonmul  21989  mplcoe1  21990  mplcoe3  21991  mplcoe5  21993  evlslem3  22033  mhpsclcl  22088  psdfval  22099  psdmplcl  22103  psdmul  22107  psdmvr  22110  coe1tm  22213  coe1tmfv2  22215  gsummoncoe1  22250  mat1comp  22382  mamulid  22383  mamurid  22384  mat1ov  22390  mattpos1  22398  mat1dimid  22416  scmateALT  22454  scmatscm  22455  1mavmul  22490  marrepval  22504  marrepeval  22505  marepvval  22509  ma1repveval  22513  1marepvmarrepid  22517  mdetdiagid  22542  mdetunilem8  22561  mdetunilem9  22562  maducoeval  22581  maducoeval2  22582  madutpos  22584  madugsum  22585  minmar1val  22590  minmar1eval  22591  symgmatr01lem  22595  symgmatr01  22596  gsummatr01lem3  22599  gsummatr01lem4  22600  gsummatr01  22601  m2cpm  22683  m2cpminvid2lem  22696  decpmatid  22712  monmatcollpw  22721  mp2pm2mplem4  22751  chmatval  22771  fvmptnn04if  22791  fclsval  23950  tmsxpsval2  24481  dscmet  24514  dscopn  24515  ovolicc1  25471  ovolicc  25478  i1f1lem  25644  itg11  25646  i1fpos  25661  itg2uba  25698  itg2split  25704  itg2monolem1  25705  itg2cnlem1  25716  itg2cnlem2  25717  itg2cn  25718  ibllem  25719  isibl  25720  itgeq1f  25726  itgeq1fOLD  25727  itgeq1  25728  cbvitgv  25732  itgresr  25734  iblpos  25748  itgposval  25751  i1fibl  25763  ibladdlem  25775  iblabslem  25783  itgcn  25800  coe1termlem  26217  coe1term  26218  cxpval  26627  leibpilem2  26905  leibpi  26906  prmorcht  27142  sqff1o  27146  pclogsum  27180  dchr1  27222  dchr2sum  27238  sum2dchr  27239  lgsval  27266  lgsneg  27286  lgsdilem  27289  lgsdir2  27295  lgsdir  27297  dchrisum0flblem2  27474  dchrisum0flb  27475  ostth1  27598  partfun2  32704  mptprop  32726  sgnneg  32863  indval  32881  indfval  32884  prodindf  32893  indsn  32894  fzto1st  33134  psgnfzto1st  33136  sgnsv  33191  sgnsval  33192  elrspunsn  33459  mvrvalind  33652  mplvrpmrhm  33661  esplysply  33678  esplyind  33680  smatfval  33901  1smat1  33910  ddeval1  34340  ddeval0  34341  eulerpartlemgvv  34482  signsvvfval  34684  signsvfn  34688  hashreprin  34726  circlemeth  34746  kur14  35359  ex-sategoelel  35564  mrsubrn  35656  prodeq12sdv  36361  itgeq12sdv  36362  cbvitgvw2  36391  cbvitgdavw  36424  cbvitgdavw2  36440  finxpeq1  37530  poimirlem5  37765  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  poimirlem10  37770  poimirlem11  37771  poimirlem12  37772  poimirlem15  37775  poimirlem16  37776  poimirlem17  37777  poimirlem18  37778  poimirlem19  37779  poimirlem20  37780  poimirlem21  37781  poimirlem22  37782  poimirlem23  37783  poimirlem27  37787  itg2addnclem  37811  itg2gt0cn  37815  ibladdnclem  37816  iblabsnclem  37823  ftc1anclem5  37837  ftc1anc  37841  ftc2nc  37842  frlmvscadiccat  42703  fiabv  42733  evlsbagval  42754  selvvvval  42770  fsuppind  42775  pw2f1ocnv  43221  flcidc  43354  cantnfresb  43508  refsum2cnlem1  45224  icccncfext  46073  fourierdlem112  46404  fourierswlem  46416  fouriersw  46417  etransclem1  46421  etransclem5  46425  etransclem17  46437  etransclem32  46452  etransclem41  46461  hoidmv1lelem2  46778  ovnhoi  46789  hspdifhsp  46802  hspmbl  46815  hoimbl  46817  ovnsubadd2  46832  suppmptcfin  48564  linc0scn0  48611  linc1  48613  lcoss  48624  el0ldep  48654