Theorem ifbieq1d 4572

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-un 3981  df-if 4549

This theorem is referenced by:  opeq1  4897  opeq2  4898  oieq1  9581  oieq2  9582  cantnflem1d  9757  cantnflem1  9758  ttrcltr  9785  iunfictbso  10183  ttukey2g  10585  bcval  14353  swrdval  14691  summolem2a  15763  zsum  15766  fsum  15768  sumss  15772  sumss2  15774  fsumcvg2  15775  fsumser  15778  isumless  15893  cbvprod  15961  cbvprodv  15962  prodmolem2a  15982  zprod  15985  fprod  15989  fprodntriv  15990  prodss  15995  rpnnen2lem1  16262  sadadd2lem  16505  sadadd2  16506  pcmpt  16939  pcmptdvds  16941  prmreclem2  16964  prmreclem4  16966  prmreclem5  16967  prmreclem6  16968  prmrec  16969  ramub1lem2  17074  ramcl  17076  prmop1  17085  prmonn2  17086  prmdvdsprmo  17089  fvprmselelfz  17091  fvprmselgcd1  17092  prmodvdslcmf  17094  prmgapprmo  17109  smndex2dlinvh  18952  pmtrval  19493  pmtrdifellem3  19520  cyggenod2  19927  gsummpt1n0  20007  dmdprdsplitlem  20081  cycsubggenodd  20153  cyggic  21614  evlslem2  22126  coe1tmmul2fv  22302  coe1pwmulfv  22304  dmatmulcl  22527  scmatscmiddistr  22535  marrepval  22589  maducoeval  22666  maducoeval2  22667  minmar1val  22675  fclsval  24037  stdbdmetval  24548  stdbdxmet  24549  pcopt2  25075  cmetcaulem  25341  ovolicc2lem3  25573  ovolicc2lem4  25574  ovolicc2lem5  25575  mbfposb  25707  i1fres  25760  i1fposd  25762  mbfi1fseqlem2  25771  mbfi1fseq  25776  mbfi1flimlem  25777  mbfi1flim  25778  itg2splitlem  25803  itg2cnlem1  25816  itg2cn  25818  isibl  25820  isibl2  25821  iblitg  25823  dfitg  25824  cbvitg  25831  itgeq2  25833  itgvallem  25840  iblneg  25858  itgneg  25859  itgss3  25870  itgcn  25900  deg1suble  26166  elply2  26255  dgrsub  26332  aareccl  26386  vmaval  27174  prmorcht  27239  pclogsum  27277  dchrelbasd  27301  dchrptlem2  27327  bposlem5  27350  lgsfval  27364  lgsdir  27394  lgsdilem2  27395  lgsdi  27396  lgsne0  27397  rplogsumlem2  27547  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  elrspunsn  33422  gsummoncoe1fzo  33583  ballotlemsval  34473  ballotlemieq  34481  mrsubfval  35476  cbvprodvw2  36213  cbvproddavw  36246  cbvsumdavw2  36261  cbvproddavw2  36262  poimirlem1  37581  poimirlem5  37585  poimirlem6  37586  poimirlem12  37592  poimirlem22  37602  mblfinlem2  37618  itg2addnclem  37631  ftc1anclem5  37657  ftc1anclem6  37658  cdlemk40  40874  fsuppind  42545  cantnfub  43283  dvnprodlem1  45867  fourierdlem86  46113  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  isomennd  46452  hsphoif  46497  hsphoival  46500  sge0hsphoire  46510  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hoidmvlelem5  46520  hspval  46530  hoidifhspval2  46536  hoidifhspval3  46540  hspmbllem2  46548  afveq12d  47048