Theorem ifbieq1d 4552

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ifcif 4528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-un 3953  df-if 4529

This theorem is referenced by:  opeq1  4873  opeq2  4874  oieq1  9509  oieq2  9510  cantnflem1d  9685  cantnflem1  9686  ttrcltr  9713  iunfictbso  10111  ttukey2g  10513  bcval  14268  swrdval  14597  summolem2a  15665  zsum  15668  fsum  15670  sumss  15674  sumss2  15676  fsumcvg2  15677  fsumser  15680  isumless  15795  cbvprod  15863  prodmolem2a  15882  zprod  15885  fprod  15889  fprodntriv  15890  prodss  15895  rpnnen2lem1  16161  sadadd2lem  16404  sadadd2  16405  pcmpt  16829  pcmptdvds  16831  prmreclem2  16854  prmreclem4  16856  prmreclem5  16857  prmreclem6  16858  prmrec  16859  ramub1lem2  16964  ramcl  16966  prmop1  16975  prmonn2  16976  prmdvdsprmo  16979  fvprmselelfz  16981  fvprmselgcd1  16982  prmodvdslcmf  16984  prmgapprmo  16999  smndex2dlinvh  18834  pmtrval  19360  pmtrdifellem3  19387  cyggenod2  19794  gsummpt1n0  19874  dmdprdsplitlem  19948  cycsubggenodd  20020  cyggic  21347  evlslem2  21861  coe1tmmul2fv  22020  coe1pwmulfv  22022  dmatmulcl  22222  scmatscmiddistr  22230  marrepval  22284  maducoeval  22361  maducoeval2  22362  minmar1val  22370  fclsval  23732  stdbdmetval  24243  stdbdxmet  24244  pcopt2  24763  cmetcaulem  25029  ovolicc2lem3  25260  ovolicc2lem4  25261  ovolicc2lem5  25262  mbfposb  25394  i1fres  25447  i1fposd  25449  mbfi1fseqlem2  25458  mbfi1fseq  25463  mbfi1flimlem  25464  mbfi1flim  25465  itg2splitlem  25490  itg2cnlem1  25503  itg2cn  25505  isibl  25507  isibl2  25508  iblitg  25510  dfitg  25511  cbvitg  25517  itgeq2  25519  itgvallem  25526  iblneg  25544  itgneg  25545  itgss3  25556  itgcn  25586  deg1suble  25849  elply2  25934  dgrsub  26010  aareccl  26063  vmaval  26841  prmorcht  26906  pclogsum  26942  dchrelbasd  26966  dchrptlem2  26992  bposlem5  27015  lgsfval  27029  lgsdir  27059  lgsdilem2  27060  lgsdi  27061  lgsne0  27062  rplogsumlem2  27212  pntrlog2bndlem4  27307  pntrlog2bndlem5  27308  elrspunsn  32809  gsummoncoe1fzo  32931  ballotlemsval  33793  ballotlemieq  33801  mrsubfval  34785  poimirlem1  36792  poimirlem5  36796  poimirlem6  36797  poimirlem12  36803  poimirlem22  36813  mblfinlem2  36829  itg2addnclem  36842  ftc1anclem5  36868  ftc1anclem6  36869  cdlemk40  40091  fsuppind  41464  cantnfub  42373  dvnprodlem1  44961  fourierdlem86  45207  fourierdlem97  45218  fourierdlem103  45224  fourierdlem104  45225  fourierdlem112  45233  isomennd  45546  hsphoif  45591  hsphoival  45594  sge0hsphoire  45604  hoidmv1lelem2  45607  hoidmv1lelem3  45608  hoidmv1le  45609  hoidmvlelem1  45610  hoidmvlelem2  45611  hoidmvlelem3  45612  hoidmvlelem4  45613  hoidmvlelem5  45614  hspval  45624  hoidifhspval2  45630  hoidifhspval3  45634  hspmbllem2  45642  afveq12d  46140