Theorem ifbieq1d 4449

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-un 3858  df-if 4426

This theorem is referenced by:  opeq1  4770  opeq2  4771  oieq1  9106  oieq2  9107  cantnflem1d  9281  cantnflem1  9282  iunfictbso  9693  ttukey2g  10095  bcval  13835  swrdval  14173  summolem2a  15244  zsum  15247  fsum  15249  sumss  15253  sumss2  15255  fsumcvg2  15256  fsumser  15259  isumless  15372  cbvprod  15440  prodmolem2a  15459  zprod  15462  fprod  15466  fprodntriv  15467  prodss  15472  rpnnen2lem1  15738  sadadd2lem  15981  sadadd2  15982  pcmpt  16408  pcmptdvds  16410  prmreclem2  16433  prmreclem4  16435  prmreclem5  16436  prmreclem6  16437  prmrec  16438  ramub1lem2  16543  ramcl  16545  prmop1  16554  prmonn2  16555  prmdvdsprmo  16558  fvprmselelfz  16560  fvprmselgcd1  16561  prmodvdslcmf  16563  prmgapprmo  16578  smndex2dlinvh  18298  pmtrval  18797  pmtrdifellem3  18824  cyggenod2  19223  gsummpt1n0  19304  dmdprdsplitlem  19378  cycsubggenodd  19450  cyggic  20491  evlslem2  20993  coe1tmmul2fv  21153  coe1pwmulfv  21155  dmatmulcl  21351  scmatscmiddistr  21359  marrepval  21413  maducoeval  21490  maducoeval2  21491  minmar1val  21499  fclsval  22859  stdbdmetval  23366  stdbdxmet  23367  pcopt2  23874  cmetcaulem  24139  ovolicc2lem3  24370  ovolicc2lem4  24371  ovolicc2lem5  24372  mbfposb  24504  i1fres  24557  i1fposd  24559  mbfi1fseqlem2  24568  mbfi1fseq  24573  mbfi1flimlem  24574  mbfi1flim  24575  itg2splitlem  24600  itg2cnlem1  24613  itg2cn  24615  isibl  24617  isibl2  24618  iblitg  24620  dfitg  24621  cbvitg  24627  itgeq2  24629  itgvallem  24636  iblneg  24654  itgneg  24655  itgss3  24666  itgcn  24696  deg1suble  24959  elply2  25044  dgrsub  25120  aareccl  25173  vmaval  25949  prmorcht  26014  pclogsum  26050  dchrelbasd  26074  dchrptlem2  26100  bposlem5  26123  lgsfval  26137  lgsdir  26167  lgsdilem2  26168  lgsdi  26169  lgsne0  26170  rplogsumlem2  26320  pntrlog2bndlem4  26415  pntrlog2bndlem5  26416  ballotlemsval  32141  ballotlemieq  32149  mrsubfval  33137  poimirlem1  35464  poimirlem5  35468  poimirlem6  35469  poimirlem12  35475  poimirlem22  35485  mblfinlem2  35501  itg2addnclem  35514  ftc1anclem5  35540  ftc1anclem6  35541  cdlemk40  38617  fsuppind  39930  dvnprodlem1  43105  fourierdlem86  43351  fourierdlem97  43362  fourierdlem103  43368  fourierdlem104  43369  fourierdlem112  43377  isomennd  43687  hsphoif  43732  hsphoival  43735  sge0hsphoire  43745  hoidmv1lelem2  43748  hoidmv1lelem3  43749  hoidmv1le  43750  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem3  43753  hoidmvlelem4  43754  hoidmvlelem5  43755  hspval  43765  hoidifhspval2  43771  hoidifhspval3  43775  hspmbllem2  43783  afveq12d  44240