Theorem ifbieq1d 4551

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ifcif 4527

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-un 3952  df-if 4528

This theorem is referenced by:  opeq1  4872  opeq2  4873  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  24770  cmetcaulem  25036  ovolicc2lem3  25268  ovolicc2lem4  25269  ovolicc2lem5  25270  mbfposb  25402  i1fres  25455  i1fposd  25457  mbfi1fseqlem2  25466  mbfi1fseq  25471  mbfi1flimlem  25472  mbfi1flim  25473  itg2splitlem  25498  itg2cnlem1  25511  itg2cn  25513  isibl  25515  isibl2  25516  iblitg  25518  dfitg  25519  cbvitg  25525  itgeq2  25527  itgvallem  25534  iblneg  25552  itgneg  25553  itgss3  25564  itgcn  25594  deg1suble  25860  elply2  25945  dgrsub  26022  aareccl  26075  vmaval  26853  prmorcht  26918  pclogsum  26954  dchrelbasd  26978  dchrptlem2  27004  bposlem5  27027  lgsfval  27041  lgsdir  27071  lgsdilem2  27072  lgsdi  27073  lgsne0  27074  rplogsumlem2  27224  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  elrspunsn  32821  gsummoncoe1fzo  32943  ballotlemsval  33805  ballotlemieq  33813  mrsubfval  34797  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  44960  fourierdlem86  45206  fourierdlem97  45217  fourierdlem103  45223  fourierdlem104  45224  fourierdlem112  45232  isomennd  45545  hsphoif  45590  hsphoival  45593  sge0hsphoire  45603  hoidmv1lelem2  45606  hoidmv1lelem3  45607  hoidmv1le  45608  hoidmvlelem1  45609  hoidmvlelem2  45610  hoidmvlelem3  45611  hoidmvlelem4  45612  hoidmvlelem5  45613  hspval  45623  hoidifhspval2  45629  hoidifhspval3  45633  hspmbllem2  45641  afveq12d  46139