Theorem ifbieq1d 4511

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568  ifcif 4486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-un 3909  df-if 4487

This theorem is referenced by:  opeq1  4837  opeq2  4838  oieq1  9473  oieq2  9474  cantnflem1d  9656  cantnflem1  9657  ttrcltr  9684  iunfictbso  10097  ttukey2g  10499  bcval  14339  swrdval  14680  summolem2a  15765  zsum  15768  fsum  15770  sumss  15774  sumss2  15776  fsumcvg2  15777  fsumser  15780  isumless  15898  cbvprod  15966  cbvprodv  15967  prodmolem2a  15987  zprod  15990  fprod  15994  fprodntriv  15995  prodss  16000  rpnnen2lem1  16269  sadadd2lem  16516  sadadd2  16517  pcmpt  16951  pcmptdvds  16953  prmreclem2  16976  prmreclem4  16978  prmreclem5  16979  prmreclem6  16980  prmrec  16981  ramub1lem2  17086  ramcl  17088  prmop1  17097  prmonn2  17098  prmdvdsprmo  17101  fvprmselelfz  17103  fvprmselgcd1  17104  prmodvdslcmf  17106  prmgapprmo  17121  smndex2dlinvh  18978  pmtrval  19520  pmtrdifellem3  19547  cyggenod2  19954  gsummpt1n0  20034  dmdprdsplitlem  20108  cycsubggenodd  20180  cyggic  21701  evlslem2  22209  coe1tmmul2fv  22418  coe1pwmulfv  22420  dmatmulcl  22636  scmatscmiddistr  22644  marrepval  22698  maducoeval  22775  maducoeval2  22776  minmar1val  22784  fclsval  24144  stdbdmetval  24650  stdbdxmet  24651  pcopt2  25161  cmetcaulem  25426  ovolicc2lem3  25657  ovolicc2lem4  25658  ovolicc2lem5  25659  mbfposb  25791  i1fres  25843  i1fposd  25845  mbfi1fseqlem2  25854  mbfi1fseq  25859  mbfi1flimlem  25860  mbfi1flim  25861  itg2splitlem  25886  itg2cnlem1  25899  itg2cn  25901  isibl  25903  isibl2  25904  iblitg  25906  dfitg  25907  cbvitg  25914  itgeq2  25916  itgvallem  25923  iblneg  25941  itgneg  25942  itgss3  25953  itgcn  25983  deg1suble  26243  elply2  26332  dgrsub  26408  aareccl  26466  vmaval  27253  prmorcht  27318  pclogsum  27355  dchrelbasd  27379  dchrptlem2  27405  bposlem5  27428  lgsfval  27442  lgsdir  27472  lgsdilem2  27473  lgsdi  27474  lgsne0  27475  rplogsumlem2  27625  pntrlog2bndlem4  27720  pntrlog2bndlem5  27721  elrspunsn  33703  gsummoncoe1fzo  33853  selvply1rhmlem2  33877  extvfval  33888  extvfvv  33890  fldextrspunlsp  34030  extdgfialglem2  34049  ballotlemsval  34865  ballotlemieq  34873  mrsubfval  35954  cbvprodvw2  36703  cbvproddavw  36736  cbvsumdavw2  36751  cbvproddavw2  36752  poimirlem1  38216  poimirlem5  38220  poimirlem6  38221  poimirlem12  38227  poimirlem22  38237  mblfinlem2  38253  itg2addnclem  38266  ftc1anclem5  38292  ftc1anclem6  38293  cdlemk40  41637  fsuppind  43270  cantnfub  43996  dvnprodlem1  46608  fourierdlem86  46854  fourierdlem97  46865  fourierdlem103  46871  fourierdlem104  46872  fourierdlem112  46880  isomennd  47193  hsphoif  47238  hsphoival  47241  sge0hsphoire  47251  hoidmv1lelem2  47254  hoidmv1lelem3  47255  hoidmv1le  47256  hoidmvlelem1  47257  hoidmvlelem2  47258  hoidmvlelem3  47259  hoidmvlelem4  47260  hoidmvlelem5  47261  hspval  47271  hoidifhspval2  47277  hoidifhspval3  47281  hspmbllem2  47289  afveq12d  47815  discsubc  49787  oppfvalg  49849