Theorem ifbieq1d 4507

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562  ifcif 4482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-un 3911  df-if 4483

This theorem is referenced by:  opeq1  4833  opeq2  4834  oieq1  9462  oieq2  9463  cantnflem1d  9645  cantnflem1  9646  ttrcltr  9673  iunfictbso  10072  ttukey2g  10475  bcval  14319  swrdval  14659  summolem2a  15744  zsum  15747  fsum  15749  sumss  15753  sumss2  15755  fsumcvg2  15756  fsumser  15759  isumless  15877  cbvprod  15945  cbvprodv  15946  prodmolem2a  15966  zprod  15969  fprod  15973  fprodntriv  15974  prodss  15979  rpnnen2lem1  16248  sadadd2lem  16495  sadadd2  16496  pcmpt  16930  pcmptdvds  16932  prmreclem2  16955  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  prmrec  16960  ramub1lem2  17065  ramcl  17067  prmop1  17076  prmonn2  17077  prmdvdsprmo  17080  fvprmselelfz  17082  fvprmselgcd1  17083  prmodvdslcmf  17085  prmgapprmo  17100  smndex2dlinvh  18956  pmtrval  19493  pmtrdifellem3  19520  cyggenod2  19927  gsummpt1n0  20007  dmdprdsplitlem  20081  cycsubggenodd  20153  cyggic  21626  evlslem2  22134  coe1tmmul2fv  22343  coe1pwmulfv  22345  dmatmulcl  22562  scmatscmiddistr  22570  marrepval  22624  maducoeval  22701  maducoeval2  22702  minmar1val  22710  fclsval  24070  stdbdmetval  24576  stdbdxmet  24577  pcopt2  25087  cmetcaulem  25352  ovolicc2lem3  25583  ovolicc2lem4  25584  ovolicc2lem5  25585  mbfposb  25717  i1fres  25769  i1fposd  25771  mbfi1fseqlem2  25780  mbfi1fseq  25785  mbfi1flimlem  25786  mbfi1flim  25787  itg2splitlem  25812  itg2cnlem1  25825  itg2cn  25827  isibl  25829  isibl2  25830  iblitg  25832  dfitg  25833  cbvitg  25840  itgeq2  25842  itgvallem  25849  iblneg  25867  itgneg  25868  itgss3  25879  itgcn  25909  deg1suble  26169  elply2  26258  dgrsub  26334  aareccl  26392  vmaval  27179  prmorcht  27244  pclogsum  27281  dchrelbasd  27305  dchrptlem2  27331  bposlem5  27354  lgsfval  27368  lgsdir  27398  lgsdilem2  27399  lgsdi  27400  lgsne0  27401  rplogsumlem2  27551  pntrlog2bndlem4  27646  pntrlog2bndlem5  27647  elrspunsn  33617  gsummoncoe1fzo  33795  selvply1rhmlem2  33820  extvfval  33831  extvfvv  33833  fldextrspunlsp  33973  extdgfialglem2  33992  ballotlemsval  34808  ballotlemieq  34816  mrsubfval  35863  cbvprodvw2  36612  cbvproddavw  36645  cbvsumdavw2  36660  cbvproddavw2  36661  poimirlem1  38125  poimirlem5  38129  poimirlem6  38130  poimirlem12  38136  poimirlem22  38146  mblfinlem2  38162  itg2addnclem  38175  ftc1anclem5  38201  ftc1anclem6  38202  cdlemk40  41546  fsuppind  43177  cantnfub  43903  dvnprodlem1  46525  fourierdlem86  46771  fourierdlem97  46782  fourierdlem103  46788  fourierdlem104  46789  fourierdlem112  46797  isomennd  47110  hsphoif  47155  hsphoival  47158  sge0hsphoire  47168  hoidmv1lelem2  47171  hoidmv1lelem3  47172  hoidmv1le  47173  hoidmvlelem1  47174  hoidmvlelem2  47175  hoidmvlelem3  47176  hoidmvlelem4  47177  hoidmvlelem5  47178  hspval  47188  hoidifhspval2  47194  hoidifhspval3  47198  hspmbllem2  47206  afveq12d  47732  discsubc  49690  oppfvalg  49752