Theorem ifbid 4511

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ifcif 4487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4488

This theorem is referenced by:  ifbieq1d  4512  ifbieq2d  4514  ifbieq12d  4516  ifbieq12d2  4522  ifan  4541  ifor  4542  rabsnif  4689  suppsnop  8170  resixpfo  8930  pw2f1olem  9065  unxpdomlem1  9212  cantnflem1d  9653  cantnflem1  9654  ssttrcl  9680  ttrclselem2  9691  dfac12lem1  10123  ttukeylem3  10490  indval  12216  indfval  12220  2resupmax  13209  xaddval  13244  xmulcom  13287  xmulneg1  13290  repswswrd  14817  ccatco  14868  sgnval  15121  sgnneg  15133  sumeq1  15736  sumsplit  15815  prodeq1f  15956  prodeq1  15957  rpnnen2lem1  16265  rpnnen2lem2  16266  rpnnen2lem10  16274  sadadd2lem2  16503  sadfval  16505  sadcp1  16508  sadadd2lem  16512  sadcom  16516  pcmpt  16947  pcmpt2  16948  pcfac  16954  prmrec  16977  ramcl  17084  acsfn  17710  setcepi  18140  mgmnsgrpex  18988  sgrpnmndex  18989  frgpup3lem  19842  dpjrid  20129  abvtrivd  20935  obsip  21871  uvcval  21935  uvcvval  21936  psrlidm  22111  psrridm  22112  psrascl  22128  mvrval  22131  mvrval2  22132  mvrf1  22135  mplmonmul  22187  mplcoe1  22188  mplcoe3  22189  mplcoe5  22191  evlslem3  22231  selvvvval  22293  mhpsclcl  22310  psdfval  22321  psdmplcl  22325  psdmul  22329  psdmvr  22332  coe1tm  22434  coe1tmfv2  22436  gsummoncoe1  22468  mat1comp  22597  mamulid  22598  mamurid  22599  mat1ov  22605  mattpos1  22613  mat1dimid  22631  scmateALT  22669  scmatscm  22670  1mavmul  22705  marrepval  22719  marrepeval  22720  marepvval  22724  ma1repveval  22728  1marepvmarrepid  22732  mdetdiagid  22757  mdetunilem8  22776  mdetunilem9  22777  maducoeval  22796  maducoeval2  22797  madutpos  22799  madugsum  22800  minmar1val  22805  minmar1eval  22806  symgmatr01lem  22810  symgmatr01  22811  gsummatr01lem3  22814  gsummatr01lem4  22815  gsummatr01  22816  m2cpm  22898  m2cpminvid2lem  22911  decpmatid  22927  monmatcollpw  22936  mp2pm2mplem4  22966  chmatval  22986  fvmptnn04if  23006  fclsval  24165  tmsxpsval2  24696  dscmet  24729  dscopn  24730  ovolicc1  25675  ovolicc  25682  i1f1lem  25848  itg11  25850  i1fpos  25865  itg2uba  25902  itg2split  25908  itg2monolem1  25909  itg2cnlem1  25920  itg2cnlem2  25921  itg2cn  25922  ibllem  25923  isibl  25924  itgeq1f  25930  itgeq1fOLD  25931  itgeq1  25932  cbvitgv  25936  itgresr  25938  iblpos  25952  itgposval  25955  i1fibl  25967  ibladdlem  25979  iblabslem  25987  itgcn  26004  coe1termlem  26415  coe1term  26416  cxpval  26829  leibpilem2  27106  leibpi  27107  prmorcht  27342  sqff1o  27346  pclogsum  27379  dchr1  27421  dchr2sum  27437  sum2dchr  27438  lgsval  27465  lgsneg  27485  lgsdilem  27488  lgsdir2  27494  lgsdir  27496  dchrisum0flblem2  27673  dchrisum0flb  27674  ostth1  27797  partfun2  33021  mptprop  33043  prodindf  33182  indsn  33183  fzto1st  33423  psgnfzto1st  33425  sgnsv  33480  sgnsval  33481  elrspunsn  33737  mvrvalind  33928  mplvrpmrhm  33937  psrmonmul  33940  psrmonmul2  33941  psrmonprod  33942  mplmonprod  33944  esplysply  33961  esplyfval1  33963  esplyfvaln  33964  esplyind  33965  smatfval  34185  1smat1  34194  ddeval1  34624  ddeval0  34625  eulerpartlemgvv  34766  signsvvfval  34965  signsvfn  34969  hashreprin  35007  circlemeth  35027  kur14  35708  ex-sategoelel  35913  mrsubrn  36005  prodeq12sdv  36750  itgeq12sdv  36751  cbvitgvw2  36780  cbvitgdavw  36813  cbvitgdavw2  36829  finxpeq1  38052  poimirlem5  38296  poimirlem6  38297  poimirlem7  38298  poimirlem8  38299  poimirlem10  38301  poimirlem11  38302  poimirlem12  38303  poimirlem15  38306  poimirlem16  38307  poimirlem17  38308  poimirlem18  38309  poimirlem19  38310  poimirlem20  38311  poimirlem21  38312  poimirlem22  38313  poimirlem23  38314  poimirlem27  38318  itg2addnclem  38342  itg2gt0cn  38346  ibladdnclem  38347  iblabsnclem  38354  ftc1anclem5  38368  ftc1anc  38372  ftc2nc  38373  frlmvscadiccat  43300  fiabv  43324  evlsbagval  43338  fsuppind  43342  pw2f1ocnv  43784  flcidc  43917  cantnfresb  44071  refsum2cnlem1  45777  icccncfext  46621  fourierdlem112  46952  fourierswlem  46964  fouriersw  46965  etransclem1  46969  etransclem5  46973  etransclem17  46985  etransclem32  47000  etransclem41  47009  hoidmv1lelem2  47326  ovnhoi  47337  hspdifhsp  47350  hspmbl  47363  hoimbl  47365  ovnsubadd2  47380  suppmptcfin  49176  linc0scn0  49223  linc1  49225  lcoss  49236  el0ldep  49266