Theorem ifbid 4515

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  ifbieq1d  4516  ifbieq2d  4518  ifbieq12d  4520  ifbieq12d2  4526  ifan  4545  ifor  4546  rabsnif  4690  suppsnop  8160  resixpfo  8912  pw2f1olem  9050  unxpdomlem1  9204  cantnflem1d  9648  cantnflem1  9649  ssttrcl  9675  ttrclselem2  9686  dfac12lem1  10104  ttukeylem3  10471  2resupmax  13155  xaddval  13190  xmulcom  13233  xmulneg1  13236  repswswrd  14756  ccatco  14808  sgnval  15061  sumeq1  15662  sumsplit  15741  prodeq1f  15879  prodeq1  15880  rpnnen2lem1  16189  rpnnen2lem2  16190  rpnnen2lem10  16198  sadadd2lem2  16427  sadfval  16429  sadcp1  16432  sadadd2lem  16436  sadcom  16440  pcmpt  16870  pcmpt2  16871  pcfac  16877  prmrec  16900  ramcl  17007  acsfn  17627  setcepi  18057  mgmnsgrpex  18865  sgrpnmndex  18866  frgpup3lem  19714  dpjrid  20001  abvtrivd  20748  obsip  21637  uvcval  21701  uvcvval  21702  psrlidm  21878  psrridm  21879  psrascl  21895  mvrval  21898  mvrval2  21899  mvrf1  21902  mplmonmul  21950  mplcoe1  21951  mplcoe3  21952  mplcoe5  21954  evlslem3  21994  mhpsclcl  22041  psdfval  22052  psdmplcl  22056  psdmul  22060  psdmvr  22063  coe1tm  22166  coe1tmfv2  22168  gsummoncoe1  22202  mat1comp  22334  mamulid  22335  mamurid  22336  mat1ov  22342  mattpos1  22350  mat1dimid  22368  scmateALT  22406  scmatscm  22407  1mavmul  22442  marrepval  22456  marrepeval  22457  marepvval  22461  ma1repveval  22465  1marepvmarrepid  22469  mdetdiagid  22494  mdetunilem8  22513  mdetunilem9  22514  maducoeval  22533  maducoeval2  22534  madutpos  22536  madugsum  22537  minmar1val  22542  minmar1eval  22543  symgmatr01lem  22547  symgmatr01  22548  gsummatr01lem3  22551  gsummatr01lem4  22552  gsummatr01  22553  m2cpm  22635  m2cpminvid2lem  22648  decpmatid  22664  monmatcollpw  22673  mp2pm2mplem4  22703  chmatval  22723  fvmptnn04if  22743  fclsval  23902  tmsxpsval2  24434  dscmet  24467  dscopn  24468  ovolicc1  25424  ovolicc  25431  i1f1lem  25597  itg11  25599  i1fpos  25614  itg2uba  25651  itg2split  25657  itg2monolem1  25658  itg2cnlem1  25669  itg2cnlem2  25670  itg2cn  25671  ibllem  25672  isibl  25673  itgeq1f  25679  itgeq1fOLD  25680  itgeq1  25681  cbvitgv  25685  itgresr  25687  iblpos  25701  itgposval  25704  i1fibl  25716  ibladdlem  25728  iblabslem  25736  itgcn  25753  coe1termlem  26170  coe1term  26171  cxpval  26580  leibpilem2  26858  leibpi  26859  prmorcht  27095  sqff1o  27099  pclogsum  27133  dchr1  27175  dchr2sum  27191  sum2dchr  27192  lgsval  27219  lgsneg  27239  lgsdilem  27242  lgsdir2  27248  lgsdir  27250  dchrisum0flblem2  27427  dchrisum0flb  27428  ostth1  27551  mptprop  32628  sgnneg  32765  indval  32783  indfval  32786  prodindf  32793  fzto1st  33067  psgnfzto1st  33069  sgnsv  33124  sgnsval  33125  elrspunsn  33407  smatfval  33792  1smat1  33801  ddeval1  34231  ddeval0  34232  eulerpartlemgvv  34374  signsvvfval  34576  signsvfn  34580  hashreprin  34618  circlemeth  34638  kur14  35210  ex-sategoelel  35415  mrsubrn  35507  prodeq12sdv  36213  itgeq12sdv  36214  cbvitgvw2  36243  cbvitgdavw  36276  cbvitgdavw2  36292  finxpeq1  37381  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem27  37648  itg2addnclem  37672  itg2gt0cn  37676  ibladdnclem  37677  iblabsnclem  37684  ftc1anclem5  37698  ftc1anc  37702  ftc2nc  37703  frlmvscadiccat  42501  fiabv  42531  evlsbagval  42561  selvvvval  42580  fsuppind  42585  pw2f1ocnv  43033  flcidc  43166  cantnfresb  43320  refsum2cnlem1  45038  icccncfext  45892  fourierdlem112  46223  fourierswlem  46235  fouriersw  46236  etransclem1  46240  etransclem5  46244  etransclem17  46256  etransclem32  46271  etransclem41  46280  hoidmv1lelem2  46597  ovnhoi  46608  hspdifhsp  46621  hspmbl  46634  hoimbl  46636  ovnsubadd2  46651  suppmptcfin  48368  linc0scn0  48416  linc1  48418  lcoss  48429  el0ldep  48459