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  32641  sgnneg  32779  indval  32797  indfval  32800  prodindf  32807  fzto1st  33046  psgnfzto1st  33048  sgnsv  33103  sgnsval  33104  elrspunsn  33367  smatfval  33768  1smat1  33777  ddeval1  34207  ddeval0  34208  eulerpartlemgvv  34350  signsvvfval  34552  signsvfn  34556  hashreprin  34594  circlemeth  34614  kur14  35199  ex-sategoelel  35404  mrsubrn  35496  prodeq12sdv  36202  itgeq12sdv  36203  cbvitgvw2  36232  cbvitgdavw  36265  cbvitgdavw2  36281  finxpeq1  37370  poimirlem5  37615  poimirlem6  37616  poimirlem7  37617  poimirlem8  37618  poimirlem10  37620  poimirlem11  37621  poimirlem12  37622  poimirlem15  37625  poimirlem16  37626  poimirlem17  37627  poimirlem18  37628  poimirlem19  37629  poimirlem20  37630  poimirlem21  37631  poimirlem22  37632  poimirlem23  37633  poimirlem27  37637  itg2addnclem  37661  itg2gt0cn  37665  ibladdnclem  37666  iblabsnclem  37673  ftc1anclem5  37687  ftc1anc  37691  ftc2nc  37692  frlmvscadiccat  42489  fiabv  42519  evlsbagval  42549  selvvvval  42568  fsuppind  42573  pw2f1ocnv  43020  flcidc  43153  cantnfresb  43307  refsum2cnlem1  45025  icccncfext  45878  fourierdlem112  46209  fourierswlem  46221  fouriersw  46222  etransclem1  46226  etransclem5  46230  etransclem17  46242  etransclem32  46257  etransclem41  46266  hoidmv1lelem2  46583  ovnhoi  46594  hspdifhsp  46607  hspmbl  46620  hoimbl  46622  ovnsubadd2  46637  suppmptcfin  48370  linc0scn0  48418  linc1  48420  lcoss  48431  el0ldep  48461