Theorem ifbid 4500

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4477

This theorem is referenced by:  ifbieq1d  4501  ifbieq2d  4503  ifbieq12d  4505  ifbieq12d2  4511  ifan  4530  ifor  4531  rabsnif  4675  suppsnop  8111  resixpfo  8863  pw2f1olem  8998  unxpdomlem1  9145  cantnflem1d  9584  cantnflem1  9585  ssttrcl  9611  ttrclselem2  9622  dfac12lem1  10038  ttukeylem3  10405  2resupmax  13090  xaddval  13125  xmulcom  13168  xmulneg1  13171  repswswrd  14690  ccatco  14742  sgnval  14995  sumeq1  15596  sumsplit  15675  prodeq1f  15813  prodeq1  15814  rpnnen2lem1  16123  rpnnen2lem2  16124  rpnnen2lem10  16132  sadadd2lem2  16361  sadfval  16363  sadcp1  16366  sadadd2lem  16370  sadcom  16374  pcmpt  16804  pcmpt2  16805  pcfac  16811  prmrec  16834  ramcl  16941  acsfn  17565  setcepi  17995  mgmnsgrpex  18805  sgrpnmndex  18806  frgpup3lem  19656  dpjrid  19943  abvtrivd  20717  obsip  21628  uvcval  21692  uvcvval  21693  psrlidm  21869  psrridm  21870  psrascl  21886  mvrval  21889  mvrval2  21890  mvrf1  21893  mplmonmul  21941  mplcoe1  21942  mplcoe3  21943  mplcoe5  21945  evlslem3  21985  mhpsclcl  22032  psdfval  22043  psdmplcl  22047  psdmul  22051  psdmvr  22054  coe1tm  22157  coe1tmfv2  22159  gsummoncoe1  22193  mat1comp  22325  mamulid  22326  mamurid  22327  mat1ov  22333  mattpos1  22341  mat1dimid  22359  scmateALT  22397  scmatscm  22398  1mavmul  22433  marrepval  22447  marrepeval  22448  marepvval  22452  ma1repveval  22456  1marepvmarrepid  22460  mdetdiagid  22485  mdetunilem8  22504  mdetunilem9  22505  maducoeval  22524  maducoeval2  22525  madutpos  22527  madugsum  22528  minmar1val  22533  minmar1eval  22534  symgmatr01lem  22538  symgmatr01  22539  gsummatr01lem3  22542  gsummatr01lem4  22543  gsummatr01  22544  m2cpm  22626  m2cpminvid2lem  22639  decpmatid  22655  monmatcollpw  22664  mp2pm2mplem4  22694  chmatval  22714  fvmptnn04if  22734  fclsval  23893  tmsxpsval2  24425  dscmet  24458  dscopn  24459  ovolicc1  25415  ovolicc  25422  i1f1lem  25588  itg11  25590  i1fpos  25605  itg2uba  25642  itg2split  25648  itg2monolem1  25649  itg2cnlem1  25660  itg2cnlem2  25661  itg2cn  25662  ibllem  25663  isibl  25664  itgeq1f  25670  itgeq1fOLD  25671  itgeq1  25672  cbvitgv  25676  itgresr  25678  iblpos  25692  itgposval  25695  i1fibl  25707  ibladdlem  25719  iblabslem  25727  itgcn  25744  coe1termlem  26161  coe1term  26162  cxpval  26571  leibpilem2  26849  leibpi  26850  prmorcht  27086  sqff1o  27090  pclogsum  27124  dchr1  27166  dchr2sum  27182  sum2dchr  27183  lgsval  27210  lgsneg  27230  lgsdilem  27233  lgsdir2  27239  lgsdir  27241  dchrisum0flblem2  27418  dchrisum0flb  27419  ostth1  27542  mptprop  32648  sgnneg  32787  indval  32805  indfval  32808  prodindf  32815  fzto1st  33054  psgnfzto1st  33056  sgnsv  33111  sgnsval  33112  elrspunsn  33375  mplvrpmrhm  33558  smatfval  33778  1smat1  33787  ddeval1  34217  ddeval0  34218  eulerpartlemgvv  34360  signsvvfval  34562  signsvfn  34566  hashreprin  34604  circlemeth  34624  kur14  35209  ex-sategoelel  35414  mrsubrn  35506  prodeq12sdv  36212  itgeq12sdv  36213  cbvitgvw2  36242  cbvitgdavw  36275  cbvitgdavw2  36291  finxpeq1  37380  poimirlem5  37625  poimirlem6  37626  poimirlem7  37627  poimirlem8  37628  poimirlem10  37630  poimirlem11  37631  poimirlem12  37632  poimirlem15  37635  poimirlem16  37636  poimirlem17  37637  poimirlem18  37638  poimirlem19  37639  poimirlem20  37640  poimirlem21  37641  poimirlem22  37642  poimirlem23  37643  poimirlem27  37647  itg2addnclem  37671  itg2gt0cn  37675  ibladdnclem  37676  iblabsnclem  37683  ftc1anclem5  37697  ftc1anc  37701  ftc2nc  37702  frlmvscadiccat  42499  fiabv  42529  evlsbagval  42559  selvvvval  42578  fsuppind  42583  pw2f1ocnv  43030  flcidc  43163  cantnfresb  43317  refsum2cnlem1  45035  icccncfext  45888  fourierdlem112  46219  fourierswlem  46231  fouriersw  46232  etransclem1  46236  etransclem5  46240  etransclem17  46252  etransclem32  46267  etransclem41  46276  hoidmv1lelem2  46593  ovnhoi  46604  hspdifhsp  46617  hspmbl  46630  hoimbl  46632  ovnsubadd2  46647  suppmptcfin  48380  linc0scn0  48428  linc1  48430  lcoss  48441  el0ldep  48471