Theorem ifbieq1d 4504

Description: Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.)

Hypotheses

Ref	Expression
ifbieq1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
ifbieq1d.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifbieq1d	⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

Proof of Theorem ifbieq1d

Step	Hyp	Ref	Expression
1		ifbieq1d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ifbid 4503	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3		ifbieq1d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq1d 4499	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
5	2, 4	eqtrd 2771	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906  df-if 4480

This theorem is referenced by:  opeq1  4829  opeq2  4830  oieq1  9417  oieq2  9418  cantnflem1d  9597  cantnflem1  9598  ttrcltr  9625  iunfictbso  10024  ttukey2g  10426  bcval  14227  swrdval  14567  summolem2a  15638  zsum  15641  fsum  15643  sumss  15647  sumss2  15649  fsumcvg2  15650  fsumser  15653  isumless  15768  cbvprod  15836  cbvprodv  15837  prodmolem2a  15857  zprod  15860  fprod  15864  fprodntriv  15865  prodss  15870  rpnnen2lem1  16139  sadadd2lem  16386  sadadd2  16387  pcmpt  16820  pcmptdvds  16822  prmreclem2  16845  prmreclem4  16847  prmreclem5  16848  prmreclem6  16849  prmrec  16850  ramub1lem2  16955  ramcl  16957  prmop1  16966  prmonn2  16967  prmdvdsprmo  16970  fvprmselelfz  16972  fvprmselgcd1  16973  prmodvdslcmf  16975  prmgapprmo  16990  smndex2dlinvh  18842  pmtrval  19380  pmtrdifellem3  19407  cyggenod2  19814  gsummpt1n0  19894  dmdprdsplitlem  19968  cycsubggenodd  20040  cyggic  21527  evlslem2  22034  coe1tmmul2fv  22220  coe1pwmulfv  22222  dmatmulcl  22444  scmatscmiddistr  22452  marrepval  22506  maducoeval  22583  maducoeval2  22584  minmar1val  22592  fclsval  23952  stdbdmetval  24458  stdbdxmet  24459  pcopt2  24979  cmetcaulem  25244  ovolicc2lem3  25476  ovolicc2lem4  25477  ovolicc2lem5  25478  mbfposb  25610  i1fres  25662  i1fposd  25664  mbfi1fseqlem2  25673  mbfi1fseq  25678  mbfi1flimlem  25679  mbfi1flim  25680  itg2splitlem  25705  itg2cnlem1  25718  itg2cn  25720  isibl  25722  isibl2  25723  iblitg  25725  dfitg  25726  cbvitg  25733  itgeq2  25735  itgvallem  25742  iblneg  25760  itgneg  25761  itgss3  25772  itgcn  25802  deg1suble  26068  elply2  26157  dgrsub  26234  aareccl  26290  vmaval  27079  prmorcht  27144  pclogsum  27182  dchrelbasd  27206  dchrptlem2  27232  bposlem5  27255  lgsfval  27269  lgsdir  27299  lgsdilem2  27300  lgsdi  27301  lgsne0  27302  rplogsumlem2  27452  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  elrspunsn  33510  gsummoncoe1fzo  33678  extvfval  33697  extvfvv  33699  fldextrspunlsp  33831  extdgfialglem2  33850  ballotlemsval  34666  ballotlemieq  34674  mrsubfval  35702  cbvprodvw2  36441  cbvproddavw  36474  cbvsumdavw2  36489  cbvproddavw2  36490  poimirlem1  37818  poimirlem5  37822  poimirlem6  37823  poimirlem12  37829  poimirlem22  37839  mblfinlem2  37855  itg2addnclem  37868  ftc1anclem5  37894  ftc1anclem6  37895  cdlemk40  41173  fsuppind  42829  cantnfub  43559  dvnprodlem1  46186  fourierdlem86  46432  fourierdlem97  46443  fourierdlem103  46449  fourierdlem104  46450  fourierdlem112  46458  isomennd  46771  hsphoif  46816  hsphoival  46819  sge0hsphoire  46829  hoidmv1lelem2  46832  hoidmv1lelem3  46833  hoidmv1le  46834  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem3  46837  hoidmvlelem4  46838  hoidmvlelem5  46839  hspval  46849  hoidifhspval2  46855  hoidifhspval3  46859  hspmbllem2  46867  afveq12d  47375  discsubc  49305  oppfvalg  49367