Theorem ifbid 4447

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ifcif 4425

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426

This theorem is referenced by:  ifbieq1d  4448  ifbieq2d  4450  ifbieq12d  4452  ifbieq12d2  4458  ifan  4476  ifor  4477  rabsnif  4619  suppsnop  7827  resixpfo  8483  pw2f1olem  8604  unxpdomlem1  8706  cantnflem1d  9135  cantnflem1  9136  dfac12lem1  9554  ttukeylem3  9922  2resupmax  12569  xaddval  12604  xmulcom  12647  xmulneg1  12650  repswswrd  14137  ccatco  14188  sgnval  14439  sumeq1  15037  sumsplit  15115  prodeq1f  15254  rpnnen2lem1  15559  rpnnen2lem2  15560  rpnnen2lem10  15568  sadadd2lem2  15789  sadfval  15791  sadcp1  15794  sadadd2lem  15798  sadcom  15802  pcmpt  16218  pcmpt2  16219  pcfac  16225  prmrec  16248  ramcl  16355  acsfn  16922  setcepi  17340  mgmnsgrpex  18088  sgrpnmndex  18089  frgpup3lem  18895  dpjrid  19177  abvtrivd  19604  obsip  20410  uvcval  20474  uvcvval  20475  psrlidm  20641  psrridm  20642  mvrval  20659  mvrval2  20660  mvrf1  20663  mplmonmul  20704  mplcoe1  20705  mplcoe3  20706  mplcoe5  20708  evlslem3  20752  coe1tm  20902  coe1tmfv2  20904  gsummoncoe1  20933  mat1comp  21045  mamulid  21046  mamurid  21047  mat1ov  21053  mattpos1  21061  mat1dimid  21079  scmateALT  21117  scmatscm  21118  1mavmul  21153  marrepval  21167  marrepeval  21168  marepvval  21172  ma1repveval  21176  1marepvmarrepid  21180  mdetdiagid  21205  mdetunilem8  21224  mdetunilem9  21225  maducoeval  21244  maducoeval2  21245  madutpos  21247  madugsum  21248  minmar1val  21253  minmar1eval  21254  symgmatr01lem  21258  symgmatr01  21259  gsummatr01lem3  21262  gsummatr01lem4  21263  gsummatr01  21264  m2cpm  21346  m2cpminvid2lem  21359  decpmatid  21375  monmatcollpw  21384  mp2pm2mplem4  21414  chmatval  21434  fvmptnn04if  21454  fclsval  22613  tmsxpsval2  23146  dscmet  23179  dscopn  23180  ovolicc1  24120  ovolicc  24127  i1f1lem  24293  itg11  24295  i1fpos  24310  itg2uba  24347  itg2split  24353  itg2monolem1  24354  itg2cnlem1  24365  itg2cnlem2  24366  itg2cn  24367  ibllem  24368  isibl  24369  itgeq1f  24375  itgresr  24382  iblpos  24396  itgposval  24399  i1fibl  24411  ibladdlem  24423  iblabslem  24431  itgcn  24448  coe1termlem  24855  coe1term  24856  cxpval  25255  leibpilem2  25527  leibpi  25528  prmorcht  25763  sqff1o  25767  pclogsum  25799  dchr1  25841  dchr2sum  25857  sum2dchr  25858  lgsval  25885  lgsneg  25905  lgsdilem  25908  lgsdir2  25914  lgsdir  25916  dchrisum0flblem2  26093  dchrisum0flb  26094  ostth1  26217  mptprop  30458  fzto1st  30795  psgnfzto1st  30797  sgnsv  30852  sgnsval  30853  smatfval  31148  1smat1  31157  indval  31382  indfval  31385  prodindf  31392  ddeval1  31603  ddeval0  31604  eulerpartlemgvv  31744  sgnneg  31908  signsvvfval  31958  signsvfn  31962  hashreprin  32001  circlemeth  32021  kur14  32576  ex-sategoelel  32781  mrsubrn  32873  finxpeq1  34803  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem23  35080  poimirlem27  35084  itg2addnclem  35108  itg2gt0cn  35112  ibladdnclem  35113  iblabsnclem  35120  ftc1anclem5  35134  ftc1anc  35138  ftc2nc  35139  metakunt11  39360  metakunt32  39381  frlmvscadiccat  39440  fsuppind  39456  pw2f1ocnv  39978  flcidc  40118  refsum2cnlem1  41666  icccncfext  42529  fourierdlem112  42860  fourierswlem  42872  fouriersw  42873  etransclem1  42877  etransclem5  42881  etransclem17  42893  etransclem32  42908  etransclem41  42917  hoidmv1lelem2  43231  ovnhoi  43242  hspdifhsp  43255  hspmbl  43268  hoimbl  43270  ovnsubadd2  43285  suppmptcfin  44781  linc0scn0  44832  linc1  44834  lcoss  44845  el0ldep  44875