Theorem ifbid 4496

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

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4473

This theorem is referenced by:  ifbieq1d  4497  ifbieq2d  4499  ifbieq12d  4501  ifbieq12d2  4507  ifan  4526  ifor  4527  rabsnif  4673  suppsnop  8108  resixpfo  8860  pw2f1olem  8994  unxpdomlem1  9140  cantnflem1d  9578  cantnflem1  9579  ssttrcl  9605  ttrclselem2  9616  dfac12lem1  10035  ttukeylem3  10402  2resupmax  13087  xaddval  13122  xmulcom  13165  xmulneg1  13168  repswswrd  14691  ccatco  14742  sgnval  14995  sumeq1  15596  sumsplit  15675  prodeq1f  15813  prodeq1  15814  rpnnen2lem1  16123  rpnnen2lem2  16124  rpnnen2lem10  16132  sadadd2lem2  16361  sadfval  16363  sadcp1  16366  sadadd2lem  16370  sadcom  16374  pcmpt  16804  pcmpt2  16805  pcfac  16811  prmrec  16834  ramcl  16941  acsfn  17565  setcepi  17995  mgmnsgrpex  18839  sgrpnmndex  18840  frgpup3lem  19689  dpjrid  19976  abvtrivd  20747  obsip  21658  uvcval  21722  uvcvval  21723  psrlidm  21899  psrridm  21900  psrascl  21916  mvrval  21919  mvrval2  21920  mvrf1  21923  mplmonmul  21971  mplcoe1  21972  mplcoe3  21973  mplcoe5  21975  evlslem3  22015  mhpsclcl  22062  psdfval  22073  psdmplcl  22077  psdmul  22081  psdmvr  22084  coe1tm  22187  coe1tmfv2  22189  gsummoncoe1  22223  mat1comp  22355  mamulid  22356  mamurid  22357  mat1ov  22363  mattpos1  22371  mat1dimid  22389  scmateALT  22427  scmatscm  22428  1mavmul  22463  marrepval  22477  marrepeval  22478  marepvval  22482  ma1repveval  22486  1marepvmarrepid  22490  mdetdiagid  22515  mdetunilem8  22534  mdetunilem9  22535  maducoeval  22554  maducoeval2  22555  madutpos  22557  madugsum  22558  minmar1val  22563  minmar1eval  22564  symgmatr01lem  22568  symgmatr01  22569  gsummatr01lem3  22572  gsummatr01lem4  22573  gsummatr01  22574  m2cpm  22656  m2cpminvid2lem  22669  decpmatid  22685  monmatcollpw  22694  mp2pm2mplem4  22724  chmatval  22744  fvmptnn04if  22764  fclsval  23923  tmsxpsval2  24454  dscmet  24487  dscopn  24488  ovolicc1  25444  ovolicc  25451  i1f1lem  25617  itg11  25619  i1fpos  25634  itg2uba  25671  itg2split  25677  itg2monolem1  25678  itg2cnlem1  25689  itg2cnlem2  25690  itg2cn  25691  ibllem  25692  isibl  25693  itgeq1f  25699  itgeq1fOLD  25700  itgeq1  25701  cbvitgv  25705  itgresr  25707  iblpos  25721  itgposval  25724  i1fibl  25736  ibladdlem  25748  iblabslem  25756  itgcn  25773  coe1termlem  26190  coe1term  26191  cxpval  26600  leibpilem2  26878  leibpi  26879  prmorcht  27115  sqff1o  27119  pclogsum  27153  dchr1  27195  dchr2sum  27211  sum2dchr  27212  lgsval  27239  lgsneg  27259  lgsdilem  27262  lgsdir2  27268  lgsdir  27270  dchrisum0flblem2  27447  dchrisum0flb  27448  ostth1  27571  mptprop  32679  sgnneg  32816  indval  32834  indfval  32837  prodindf  32844  fzto1st  33072  psgnfzto1st  33074  sgnsv  33129  sgnsval  33130  elrspunsn  33394  mplvrpmrhm  33577  esplysply  33592  smatfval  33808  1smat1  33817  ddeval1  34247  ddeval0  34248  eulerpartlemgvv  34389  signsvvfval  34591  signsvfn  34595  hashreprin  34633  circlemeth  34653  kur14  35260  ex-sategoelel  35465  mrsubrn  35557  prodeq12sdv  36262  itgeq12sdv  36263  cbvitgvw2  36292  cbvitgdavw  36325  cbvitgdavw2  36341  finxpeq1  37430  poimirlem5  37675  poimirlem6  37676  poimirlem7  37677  poimirlem8  37678  poimirlem10  37680  poimirlem11  37681  poimirlem12  37682  poimirlem15  37685  poimirlem16  37686  poimirlem17  37687  poimirlem18  37688  poimirlem19  37689  poimirlem20  37690  poimirlem21  37691  poimirlem22  37692  poimirlem23  37693  poimirlem27  37697  itg2addnclem  37721  itg2gt0cn  37725  ibladdnclem  37726  iblabsnclem  37733  ftc1anclem5  37747  ftc1anc  37751  ftc2nc  37752  frlmvscadiccat  42609  fiabv  42639  evlsbagval  42669  selvvvval  42688  fsuppind  42693  pw2f1ocnv  43140  flcidc  43273  cantnfresb  43427  refsum2cnlem1  45144  icccncfext  45995  fourierdlem112  46326  fourierswlem  46338  fouriersw  46339  etransclem1  46343  etransclem5  46347  etransclem17  46359  etransclem32  46374  etransclem41  46383  hoidmv1lelem2  46700  ovnhoi  46711  hspdifhsp  46724  hspmbl  46737  hoimbl  46739  ovnsubadd2  46754  suppmptcfin  48486  linc0scn0  48534  linc1  48536  lcoss  48547  el0ldep  48577