Theorem ifbid 4489

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ifcif 4467

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4468

This theorem is referenced by:  ifbieq1d  4490  ifbieq2d  4492  ifbieq12d  4494  ifbieq12d2  4500  ifan  4518  ifor  4519  rabsnif  4659  suppsnop  7844  resixpfo  8500  pw2f1olem  8621  unxpdomlem1  8722  cantnflem1d  9151  cantnflem1  9152  dfac12lem1  9569  ttukeylem3  9933  2resupmax  12582  xaddval  12617  xmulcom  12660  xmulneg1  12663  repswswrd  14146  ccatco  14197  sgnval  14447  sumeq1  15045  sumsplit  15123  prodeq1f  15262  rpnnen2lem1  15567  rpnnen2lem2  15568  rpnnen2lem10  15576  sadadd2lem2  15799  sadfval  15801  sadcp1  15804  sadadd2lem  15808  sadcom  15812  pcmpt  16228  pcmpt2  16229  pcfac  16235  prmrec  16258  ramcl  16365  acsfn  16930  setcepi  17348  mgmnsgrpex  18096  sgrpnmndex  18097  frgpup3lem  18903  dpjrid  19184  abvtrivd  19611  psrlidm  20183  psrridm  20184  mvrval  20201  mvrval2  20202  mvrf1  20205  mplmonmul  20245  mplcoe1  20246  mplcoe3  20247  mplcoe5  20249  evlslem3  20293  coe1tm  20441  coe1tmfv2  20443  gsummoncoe1  20472  obsip  20865  uvcval  20929  uvcvval  20930  mat1comp  21049  mamulid  21050  mamurid  21051  mat1ov  21057  mattpos1  21065  mat1dimid  21083  scmateALT  21121  scmatscm  21122  1mavmul  21157  marrepval  21171  marrepeval  21172  marepvval  21176  ma1repveval  21180  1marepvmarrepid  21184  mdetdiagid  21209  mdetunilem8  21228  mdetunilem9  21229  maducoeval  21248  maducoeval2  21249  madutpos  21251  madugsum  21252  minmar1val  21257  minmar1eval  21258  symgmatr01lem  21262  symgmatr01  21263  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  m2cpm  21349  m2cpminvid2lem  21362  decpmatid  21378  monmatcollpw  21387  mp2pm2mplem4  21417  chmatval  21437  fvmptnn04if  21457  fclsval  22616  tmsxpsval2  23149  dscmet  23182  dscopn  23183  ovolicc1  24117  ovolicc  24124  i1f1lem  24290  itg11  24292  i1fpos  24307  itg2uba  24344  itg2split  24350  itg2monolem1  24351  itg2cnlem1  24362  itg2cnlem2  24363  itg2cn  24364  ibllem  24365  isibl  24366  itgeq1f  24372  itgresr  24379  iblpos  24393  itgposval  24396  i1fibl  24408  ibladdlem  24420  iblabslem  24428  itgcn  24443  coe1termlem  24848  coe1term  24849  cxpval  25247  leibpilem2  25519  leibpi  25520  prmorcht  25755  sqff1o  25759  pclogsum  25791  dchr1  25833  dchr2sum  25849  sum2dchr  25850  lgsval  25877  lgsneg  25897  lgsdilem  25900  lgsdir2  25906  lgsdir  25908  dchrisum0flblem2  26085  dchrisum0flb  26086  ostth1  26209  mptprop  30434  fzto1st  30745  psgnfzto1st  30747  sgnsv  30802  sgnsval  30803  smatfval  31060  1smat1  31069  indval  31272  indfval  31275  prodindf  31282  ddeval1  31493  ddeval0  31494  eulerpartlemgvv  31634  sgnneg  31798  signsvvfval  31848  signsvfn  31852  hashreprin  31891  circlemeth  31911  kur14  32463  ex-sategoelel  32668  mrsubrn  32760  finxpeq1  34670  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem27  34934  itg2addnclem  34958  itg2gt0cn  34962  ibladdnclem  34963  iblabsnclem  34970  ftc1anclem5  34986  ftc1anc  34990  ftc2nc  34991  frlmvscadiccat  39194  pw2f1ocnv  39683  flcidc  39823  refsum2cnlem1  41343  icccncfext  42219  fourierdlem112  42552  fourierswlem  42564  fouriersw  42565  etransclem1  42569  etransclem5  42573  etransclem17  42585  etransclem32  42600  etransclem41  42609  hoidmv1lelem2  42923  ovnhoi  42934  hspdifhsp  42947  hspmbl  42960  hoimbl  42962  ovnsubadd2  42977  suppmptcfin  44476  linc0scn0  44527  linc1  44529  lcoss  44540  el0ldep  44570