Theorem ifbid 4308

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  ifcif 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-if 4287

This theorem is referenced by:  ifbieq1d  4309  ifbieq2d  4311  ifbieq12d  4313  ifbieq12d2  4319  ifan  4337  ifor  4338  rabsnif  4456  suppsnop  7546  resixpfo  8186  pw2f1olem  8306  unxpdomlem1  8406  cantnflem1d  8835  cantnflem1  8836  dfac12lem1  9253  ttukeylem3  9621  2resupmax  12240  xaddval  12275  xmulcom  12317  xmulneg1  12320  repswswrd  13758  ccatco  13808  sgnval  14054  sumeq1  14645  sumsplit  14725  prodeq1f  14862  rpnnen2lem1  15166  rpnnen2lem2  15167  rpnnen2lem10  15175  sadadd2lem2  15394  sadfval  15396  sadcp1  15399  sadadd2lem  15403  sadcom  15407  pcmpt  15816  pcmpt2  15817  pcfac  15823  prmrec  15846  ramcl  15953  acsfn  16527  setcepi  16945  mgmnsgrpex  17626  sgrpnmndex  17627  frgpup3lem  18394  dpjrid  18666  abvtrivd  19047  psrlidm  19615  psrridm  19616  mvrval  19633  mvrval2  19634  mvrf1  19637  mplmonmul  19676  mplcoe1  19677  mplcoe3  19678  mplcoe5  19680  evlslem3  19725  coe1tm  19854  coe1tmfv2  19856  gsummoncoe1  19885  obsip  20279  uvcval  20338  uvcvval  20339  mat1comp  20460  mamulid  20461  mamurid  20462  mat1ov  20469  mattpos1  20477  mat1dimid  20495  scmateALT  20533  scmatscm  20534  1mavmul  20569  marrepval  20583  marrepeval  20584  marepvval  20588  ma1repveval  20592  1marepvmarrepid  20596  mdetdiagid  20621  mdetunilem8  20640  mdetunilem9  20641  maducoeval  20660  maducoeval2  20661  madutpos  20663  madugsum  20664  minmar1val  20669  minmar1eval  20670  symgmatr01lem  20675  symgmatr01  20676  gsummatr01lem3  20679  gsummatr01lem4  20680  gsummatr01  20681  m2cpm  20763  m2cpminvid2lem  20776  decpmatid  20792  monmatcollpw  20801  mp2pm2mplem4  20831  chmatval  20851  fvmptnn04if  20871  fclsval  22029  tmsxpsval2  22561  dscmet  22594  dscopn  22595  ovolicc1  23503  ovolicc  23510  i1f1lem  23676  itg11  23678  i1fpos  23693  itg2uba  23730  itg2split  23736  itg2monolem1  23737  itg2cnlem1  23748  itg2cnlem2  23749  itg2cn  23750  ibllem  23751  isibl  23752  itgeq1f  23758  itgresr  23765  iblpos  23779  itgposval  23782  i1fibl  23794  ibladdlem  23806  iblabslem  23814  itgcn  23829  coe1termlem  24234  coe1term  24235  cxpval  24630  leibpilem2  24888  leibpi  24889  prmorcht  25124  sqff1o  25128  pclogsum  25160  dchr1  25202  dchr2sum  25218  sum2dchr  25219  lgsval  25246  lgsneg  25266  lgsdilem  25269  lgsdir2  25275  lgsdir  25277  dchrisum0flblem2  25418  dchrisum0flb  25419  ostth1  25542  sgnsv  30058  sgnsval  30059  fzto1st  30184  psgnfzto1st  30186  smatfval  30192  1smat1  30201  indval  30406  indfval  30409  prodindf  30416  ddeval1  30628  ddeval0  30629  eulerpartlemgvv  30769  sgnneg  30933  signsvvfval  30986  signsvfn  30990  hashreprin  31029  circlemeth  31049  kur14  31526  mrsubrn  31738  finxpeq1  33541  poimirlem5  33729  poimirlem6  33730  poimirlem7  33731  poimirlem8  33732  poimirlem10  33734  poimirlem11  33735  poimirlem12  33736  poimirlem15  33739  poimirlem16  33740  poimirlem17  33741  poimirlem18  33742  poimirlem19  33743  poimirlem20  33744  poimirlem21  33745  poimirlem22  33746  poimirlem23  33747  poimirlem27  33751  itg2addnclem  33775  itg2gt0cn  33779  ibladdnclem  33780  iblabsnclem  33787  ftc1anclem5  33803  ftc1anc  33807  ftc2nc  33808  pw2f1ocnv  38106  flcidc  38246  refsum2cnlem1  39691  icccncfext  40581  fourierdlem112  40915  fourierswlem  40927  fouriersw  40928  etransclem1  40932  etransclem5  40936  etransclem17  40948  etransclem32  40963  etransclem41  40972  hoidmv1lelem2  41289  ovnhoi  41300  hspdifhsp  41313  hspmbl  41326  hoimbl  41328  ovnsubadd2  41343  suppmptcfin  42729  linc0scn0  42781  linc1  42783  lcoss  42794  el0ldep  42824