Theorem ifbieq1d 4550

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 4549	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3		ifbieq1d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq1d 4545	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
5	2, 4	eqtrd 2777	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-un 3956  df-if 4526

This theorem is referenced by:  opeq1  4873  opeq2  4874  oieq1  9552  oieq2  9553  cantnflem1d  9728  cantnflem1  9729  ttrcltr  9756  iunfictbso  10154  ttukey2g  10556  bcval  14343  swrdval  14681  summolem2a  15751  zsum  15754  fsum  15756  sumss  15760  sumss2  15762  fsumcvg2  15763  fsumser  15766  isumless  15881  cbvprod  15949  cbvprodv  15950  prodmolem2a  15970  zprod  15973  fprod  15977  fprodntriv  15978  prodss  15983  rpnnen2lem1  16250  sadadd2lem  16496  sadadd2  16497  pcmpt  16930  pcmptdvds  16932  prmreclem2  16955  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  prmrec  16960  ramub1lem2  17065  ramcl  17067  prmop1  17076  prmonn2  17077  prmdvdsprmo  17080  fvprmselelfz  17082  fvprmselgcd1  17083  prmodvdslcmf  17085  prmgapprmo  17100  smndex2dlinvh  18930  pmtrval  19469  pmtrdifellem3  19496  cyggenod2  19903  gsummpt1n0  19983  dmdprdsplitlem  20057  cycsubggenodd  20129  cyggic  21591  evlslem2  22103  coe1tmmul2fv  22281  coe1pwmulfv  22283  dmatmulcl  22506  scmatscmiddistr  22514  marrepval  22568  maducoeval  22645  maducoeval2  22646  minmar1val  22654  fclsval  24016  stdbdmetval  24527  stdbdxmet  24528  pcopt2  25056  cmetcaulem  25322  ovolicc2lem3  25554  ovolicc2lem4  25555  ovolicc2lem5  25556  mbfposb  25688  i1fres  25740  i1fposd  25742  mbfi1fseqlem2  25751  mbfi1fseq  25756  mbfi1flimlem  25757  mbfi1flim  25758  itg2splitlem  25783  itg2cnlem1  25796  itg2cn  25798  isibl  25800  isibl2  25801  iblitg  25803  dfitg  25804  cbvitg  25811  itgeq2  25813  itgvallem  25820  iblneg  25838  itgneg  25839  itgss3  25850  itgcn  25880  deg1suble  26146  elply2  26235  dgrsub  26312  aareccl  26368  vmaval  27156  prmorcht  27221  pclogsum  27259  dchrelbasd  27283  dchrptlem2  27309  bposlem5  27332  lgsfval  27346  lgsdir  27376  lgsdilem2  27377  lgsdi  27378  lgsne0  27379  rplogsumlem2  27529  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  elrspunsn  33457  gsummoncoe1fzo  33618  fldextrspunlsp  33724  ballotlemsval  34511  ballotlemieq  34519  mrsubfval  35513  cbvprodvw2  36248  cbvproddavw  36281  cbvsumdavw2  36296  cbvproddavw2  36297  poimirlem1  37628  poimirlem5  37632  poimirlem6  37633  poimirlem12  37639  poimirlem22  37649  mblfinlem2  37665  itg2addnclem  37678  ftc1anclem5  37704  ftc1anclem6  37705  cdlemk40  40919  fsuppind  42600  cantnfub  43334  dvnprodlem1  45961  fourierdlem86  46207  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  isomennd  46546  hsphoif  46591  hsphoival  46594  sge0hsphoire  46604  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hoidmvlelem5  46614  hspval  46624  hoidifhspval2  46630  hoidifhspval3  46634  hspmbllem2  46642  afveq12d  47145