Theorem ifbid 4491

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

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

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 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-if 4470

This theorem is referenced by:  ifbieq1d  4492  ifbieq2d  4494  ifbieq12d  4496  ifbieq12d2  4502  ifan  4520  ifor  4521  rabsnif  4661  suppsnop  7846  resixpfo  8502  pw2f1olem  8623  unxpdomlem1  8724  cantnflem1d  9153  cantnflem1  9154  dfac12lem1  9571  ttukeylem3  9935  2resupmax  12584  xaddval  12619  xmulcom  12662  xmulneg1  12665  repswswrd  14148  ccatco  14199  sgnval  14449  sumeq1  15047  sumsplit  15125  prodeq1f  15264  rpnnen2lem1  15569  rpnnen2lem2  15570  rpnnen2lem10  15578  sadadd2lem2  15801  sadfval  15803  sadcp1  15806  sadadd2lem  15810  sadcom  15814  pcmpt  16230  pcmpt2  16231  pcfac  16237  prmrec  16260  ramcl  16367  acsfn  16932  setcepi  17350  mgmnsgrpex  18098  sgrpnmndex  18099  frgpup3lem  18905  dpjrid  19186  abvtrivd  19613  psrlidm  20185  psrridm  20186  mvrval  20203  mvrval2  20204  mvrf1  20207  mplmonmul  20247  mplcoe1  20248  mplcoe3  20249  mplcoe5  20251  evlslem3  20295  coe1tm  20443  coe1tmfv2  20445  gsummoncoe1  20474  obsip  20867  uvcval  20931  uvcvval  20932  mat1comp  21051  mamulid  21052  mamurid  21053  mat1ov  21059  mattpos1  21067  mat1dimid  21085  scmateALT  21123  scmatscm  21124  1mavmul  21159  marrepval  21173  marrepeval  21174  marepvval  21178  ma1repveval  21182  1marepvmarrepid  21186  mdetdiagid  21211  mdetunilem8  21230  mdetunilem9  21231  maducoeval  21250  maducoeval2  21251  madutpos  21253  madugsum  21254  minmar1val  21259  minmar1eval  21260  symgmatr01lem  21264  symgmatr01  21265  gsummatr01lem3  21268  gsummatr01lem4  21269  gsummatr01  21270  m2cpm  21351  m2cpminvid2lem  21364  decpmatid  21380  monmatcollpw  21389  mp2pm2mplem4  21419  chmatval  21439  fvmptnn04if  21459  fclsval  22618  tmsxpsval2  23151  dscmet  23184  dscopn  23185  ovolicc1  24119  ovolicc  24126  i1f1lem  24292  itg11  24294  i1fpos  24309  itg2uba  24346  itg2split  24352  itg2monolem1  24353  itg2cnlem1  24364  itg2cnlem2  24365  itg2cn  24366  ibllem  24367  isibl  24368  itgeq1f  24374  itgresr  24381  iblpos  24395  itgposval  24398  i1fibl  24410  ibladdlem  24422  iblabslem  24430  itgcn  24445  coe1termlem  24850  coe1term  24851  cxpval  25249  leibpilem2  25521  leibpi  25522  prmorcht  25757  sqff1o  25761  pclogsum  25793  dchr1  25835  dchr2sum  25851  sum2dchr  25852  lgsval  25879  lgsneg  25899  lgsdilem  25902  lgsdir2  25908  lgsdir  25910  dchrisum0flblem2  26087  dchrisum0flb  26088  ostth1  26211  mptprop  30436  fzto1st  30747  psgnfzto1st  30749  sgnsv  30804  sgnsval  30805  smatfval  31062  1smat1  31071  indval  31274  indfval  31277  prodindf  31284  ddeval1  31495  ddeval0  31496  eulerpartlemgvv  31636  sgnneg  31800  signsvvfval  31850  signsvfn  31854  hashreprin  31893  circlemeth  31913  kur14  32465  ex-sategoelel  32670  mrsubrn  32762  finxpeq1  34669  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem23  34917  poimirlem27  34921  itg2addnclem  34945  itg2gt0cn  34949  ibladdnclem  34950  iblabsnclem  34957  ftc1anclem5  34973  ftc1anc  34977  ftc2nc  34978  frlmvscadiccat  39152  pw2f1ocnv  39641  flcidc  39781  refsum2cnlem1  41301  icccncfext  42177  fourierdlem112  42510  fourierswlem  42522  fouriersw  42523  etransclem1  42527  etransclem5  42531  etransclem17  42543  etransclem32  42558  etransclem41  42567  hoidmv1lelem2  42881  ovnhoi  42892  hspdifhsp  42905  hspmbl  42918  hoimbl  42920  ovnsubadd2  42935  suppmptcfin  44434  linc0scn0  44485  linc1  44487  lcoss  44498  el0ldep  44528