Theorem ifbid 4506

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  ifbieq1d  4507  ifbieq2d  4509  ifbieq12d  4511  ifbieq12d2  4517  ifan  4536  ifor  4537  rabsnif  4684  suppsnop  8195  resixpfo  8964  pw2f1olem  9100  unxpdomlem1  9247  cantnflem1d  9689  cantnflem1  9690  ssttrcl  9716  ttrclselem2  9727  dfac12lem1  10222  ttukeylem3  10589  indval  12323  indfval  12327  2resupmax  13318  xaddval  13353  xmulcom  13396  xmulneg1  13399  repswswrd  14935  ccatco  14986  sgnval  15241  sgnneg  15253  sumeq1  15856  sumsplit  15934  prodeq1f  16075  prodeq1  16076  rpnnen2lem1  16382  rpnnen2lem2  16383  rpnnen2lem10  16391  sadadd2lem2  16620  sadfval  16622  sadcp1  16625  sadadd2lem  16629  sadcom  16633  pcmpt  17070  pcmpt2  17071  pcfac  17077  prmrec  17100  ramcl  17207  acsfn  17833  setcepi  18263  mgmnsgrpex  19130  sgrpnmndex  19131  frgpup3lem  19991  dpjrid  20278  abvtrivd  21089  obsip  22027  uvcval  22091  uvcvval  22092  psrlidm  22269  psrridm  22270  psrascl  22286  mvrval  22289  mvrval2  22290  mvrf1  22293  mplmonmul  22345  mplcoe1  22346  mplcoe3  22347  mplcoe5  22349  evlslem3  22389  selvvvval  22451  mhpsclcl  22468  psdfval  22479  psdmplcl  22483  psdmul  22487  psdmvr  22490  coe1tm  22592  coe1tmfv2  22594  gsummoncoe1  22626  mat1comp  22755  mamulid  22756  mamurid  22757  mat1ov  22763  mattpos1  22771  mat1dimid  22789  scmateALT  22827  scmatscm  22828  1mavmul  22863  marrepval  22877  marrepeval  22878  marepvval  22882  ma1repveval  22886  1marepvmarrepid  22890  mdetdiagid  22915  mdetunilem8  22934  mdetunilem9  22935  maducoeval  22954  maducoeval2  22955  madutpos  22957  madugsum  22958  minmar1val  22963  minmar1eval  22964  symgmatr01lem  22968  symgmatr01  22969  gsummatr01lem3  22972  gsummatr01lem4  22973  gsummatr01  22974  m2cpm  23059  m2cpminvid2lem  23072  decpmatid  23088  monmatcollpw  23097  mp2pm2mplem4  23127  chmatval  23147  fvmptnn04if  23167  fclsval  24327  tmsxpsval2  24858  dscmet  24891  dscopn  24892  ovolicc1  25837  ovolicc  25844  i1f1lem  26010  itg11  26012  i1fpos  26027  itg2uba  26064  itg2split  26070  itg2monolem1  26071  itg2cnlem1  26082  itg2cnlem2  26083  itg2cn  26084  ibllem  26085  isibl  26086  itgeq1f  26092  itgeq1  26093  cbvitgv  26097  itgresr  26099  iblpos  26113  itgposval  26116  i1fibl  26128  ibladdlem  26140  iblabslem  26148  itgcn  26165  coe1termlem  26577  coe1term  26578  cxpval  26992  leibpilem2  27269  leibpi  27270  prmorcht  27505  sqff1o  27509  pclogsum  27542  dchr1  27584  dchr2sum  27600  sum2dchr  27601  lgsval  27628  lgsneg  27648  lgsdilem  27651  lgsdir2  27657  lgsdir  27659  dchrisum0flblem2  27836  dchrisum0flb  27837  ostth1  27960  partfun2  33270  mptprop  33291  prodindf  33429  indsn  33430  fzto1st  33664  psgnfzto1st  33666  sgnsv  33721  sgnsval  33722  elrspunsn  33979  mvrvalind  34170  mplvrpmrhm  34179  psrmonmul  34182  psrmonmul2  34183  psrmonprod  34184  mplmonprod  34186  esplysply  34203  esplyfval1  34205  esplyfvaln  34206  esplyind  34207  smatfval  34427  1smat1  34436  ddeval1  34867  ddeval0  34868  eulerpartlemgvv  35008  signsvvfval  35207  signsvfn  35211  hashreprin  35249  circlemeth  35269  kur14  35981  ex-sategoelel  36186  mrsubrn  36278  prodeq12sdv  37007  itgeq12sdv  37008  cbvitgvw2  37037  cbvitgdavw  37070  cbvitgdavw2  37086  finxpeq1  38309  poimirlem5  38543  poimirlem6  38544  poimirlem7  38545  poimirlem8  38546  poimirlem10  38548  poimirlem11  38549  poimirlem12  38550  poimirlem15  38553  poimirlem16  38554  poimirlem17  38555  poimirlem18  38556  poimirlem19  38557  poimirlem20  38558  poimirlem21  38559  poimirlem22  38560  poimirlem23  38561  poimirlem27  38565  itg2addnclem  38589  itg2gt0cn  38593  ibladdnclem  38594  iblabsnclem  38601  ftc1anclem5  38615  ftc1anc  38619  ftc2nc  38620  frlmvscadiccat  43573  fiabv  43600  evlsbagval  43614  fsuppind  43618  pw2f1ocnv  44043  flcidc  44171  cantnfresb  44325  refsum2cnlem1  46053  icccncfext  46896  fourierdlem112  47227  fourierswlem  47239  fouriersw  47240  etransclem1  47244  etransclem5  47248  etransclem17  47260  etransclem32  47275  etransclem41  47284  hoidmv1lelem2  47601  ovnhoi  47612  hspdifhsp  47625  hspmbl  47638  hoimbl  47640  ovnsubadd2  47655  suppmptcfin  49487  linc0scn0  49534  linc1  49536  lcoss  49547  el0ldep  49577