Theorem ifbieq1d 4491

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ifcif 4466

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-un 3894  df-if 4467

This theorem is referenced by:  opeq1  4816  opeq2  4817  oieq1  9427  oieq2  9428  cantnflem1d  9609  cantnflem1  9610  ttrcltr  9637  iunfictbso  10036  ttukey2g  10438  bcval  14266  swrdval  14606  summolem2a  15677  zsum  15680  fsum  15682  sumss  15686  sumss2  15688  fsumcvg2  15689  fsumser  15692  isumless  15810  cbvprod  15878  cbvprodv  15879  prodmolem2a  15899  zprod  15902  fprod  15906  fprodntriv  15907  prodss  15912  rpnnen2lem1  16181  sadadd2lem  16428  sadadd2  16429  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  18888  pmtrval  19426  pmtrdifellem3  19453  cyggenod2  19860  gsummpt1n0  19940  dmdprdsplitlem  20014  cycsubggenodd  20086  cyggic  21552  evlslem2  22057  coe1tmmul2fv  22243  coe1pwmulfv  22245  dmatmulcl  22465  scmatscmiddistr  22473  marrepval  22527  maducoeval  22604  maducoeval2  22605  minmar1val  22613  fclsval  23973  stdbdmetval  24479  stdbdxmet  24480  pcopt2  24990  cmetcaulem  25255  ovolicc2lem3  25486  ovolicc2lem4  25487  ovolicc2lem5  25488  mbfposb  25620  i1fres  25672  i1fposd  25674  mbfi1fseqlem2  25683  mbfi1fseq  25688  mbfi1flimlem  25689  mbfi1flim  25690  itg2splitlem  25715  itg2cnlem1  25728  itg2cn  25730  isibl  25732  isibl2  25733  iblitg  25735  dfitg  25736  cbvitg  25743  itgeq2  25745  itgvallem  25752  iblneg  25770  itgneg  25771  itgss3  25782  itgcn  25812  deg1suble  26072  elply2  26161  dgrsub  26237  aareccl  26292  vmaval  27076  prmorcht  27141  pclogsum  27178  dchrelbasd  27202  dchrptlem2  27228  bposlem5  27251  lgsfval  27265  lgsdir  27295  lgsdilem2  27296  lgsdi  27297  lgsne0  27298  rplogsumlem2  27448  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  elrspunsn  33489  gsummoncoe1fzo  33657  extvfval  33676  extvfvv  33678  fldextrspunlsp  33818  extdgfialglem2  33837  ballotlemsval  34653  ballotlemieq  34661  mrsubfval  35690  cbvprodvw2  36429  cbvproddavw  36462  cbvsumdavw2  36477  cbvproddavw2  36478  poimirlem1  37942  poimirlem5  37946  poimirlem6  37947  poimirlem12  37953  poimirlem22  37963  mblfinlem2  37979  itg2addnclem  37992  ftc1anclem5  38018  ftc1anclem6  38019  cdlemk40  41363  fsuppind  43023  cantnfub  43749  dvnprodlem1  46374  fourierdlem86  46620  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  isomennd  46959  hsphoif  47004  hsphoival  47007  sge0hsphoire  47017  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoidmvlelem5  47027  hspval  47037  hoidifhspval2  47043  hoidifhspval3  47047  hspmbllem2  47055  afveq12d  47581  discsubc  49539  oppfvalg  49601