Theorem ifbieq1d 4513

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

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

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-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-un 3919  df-if 4489

This theorem is referenced by:  opeq1  4837  opeq2  4838  oieq1  9465  oieq2  9466  cantnflem1d  9641  cantnflem1  9642  ttrcltr  9669  iunfictbso  10067  ttukey2g  10469  bcval  14269  swrdval  14608  summolem2a  15681  zsum  15684  fsum  15686  sumss  15690  sumss2  15692  fsumcvg2  15693  fsumser  15696  isumless  15811  cbvprod  15879  cbvprodv  15880  prodmolem2a  15900  zprod  15903  fprod  15907  fprodntriv  15908  prodss  15913  rpnnen2lem1  16182  sadadd2lem  16429  sadadd2  16430  pcmpt  16863  pcmptdvds  16865  prmreclem2  16888  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  prmrec  16893  ramub1lem2  16998  ramcl  17000  prmop1  17009  prmonn2  17010  prmdvdsprmo  17013  fvprmselelfz  17015  fvprmselgcd1  17016  prmodvdslcmf  17018  prmgapprmo  17033  smndex2dlinvh  18844  pmtrval  19381  pmtrdifellem3  19408  cyggenod2  19815  gsummpt1n0  19895  dmdprdsplitlem  19969  cycsubggenodd  20041  cyggic  21482  evlslem2  21986  coe1tmmul2fv  22164  coe1pwmulfv  22166  dmatmulcl  22387  scmatscmiddistr  22395  marrepval  22449  maducoeval  22526  maducoeval2  22527  minmar1val  22535  fclsval  23895  stdbdmetval  24402  stdbdxmet  24403  pcopt2  24923  cmetcaulem  25188  ovolicc2lem3  25420  ovolicc2lem4  25421  ovolicc2lem5  25422  mbfposb  25554  i1fres  25606  i1fposd  25608  mbfi1fseqlem2  25617  mbfi1fseq  25622  mbfi1flimlem  25623  mbfi1flim  25624  itg2splitlem  25649  itg2cnlem1  25662  itg2cn  25664  isibl  25666  isibl2  25667  iblitg  25669  dfitg  25670  cbvitg  25677  itgeq2  25679  itgvallem  25686  iblneg  25704  itgneg  25705  itgss3  25716  itgcn  25746  deg1suble  26012  elply2  26101  dgrsub  26178  aareccl  26234  vmaval  27023  prmorcht  27088  pclogsum  27126  dchrelbasd  27150  dchrptlem2  27176  bposlem5  27199  lgsfval  27213  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  rplogsumlem2  27396  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  elrspunsn  33400  gsummoncoe1fzo  33563  fldextrspunlsp  33669  ballotlemsval  34500  ballotlemieq  34508  mrsubfval  35495  cbvprodvw2  36235  cbvproddavw  36268  cbvsumdavw2  36283  cbvproddavw2  36284  poimirlem1  37615  poimirlem5  37619  poimirlem6  37620  poimirlem12  37626  poimirlem22  37636  mblfinlem2  37652  itg2addnclem  37665  ftc1anclem5  37691  ftc1anclem6  37692  cdlemk40  40911  fsuppind  42578  cantnfub  43310  dvnprodlem1  45944  fourierdlem86  46190  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  isomennd  46529  hsphoif  46574  hsphoival  46577  sge0hsphoire  46587  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hoidmvlelem5  46597  hspval  46607  hoidifhspval2  46613  hoidifhspval3  46617  hspmbllem2  46625  afveq12d  47134  discsubc  49053  oppfvalg  49115