Theorem ifbieq1d 4480

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-un 3888  df-if 4457

This theorem is referenced by:  opeq1  4801  opeq2  4802  oieq1  9201  oieq2  9202  cantnflem1d  9376  cantnflem1  9377  iunfictbso  9801  ttukey2g  10203  bcval  13946  swrdval  14284  summolem2a  15355  zsum  15358  fsum  15360  sumss  15364  sumss2  15366  fsumcvg2  15367  fsumser  15370  isumless  15485  cbvprod  15553  prodmolem2a  15572  zprod  15575  fprod  15579  fprodntriv  15580  prodss  15585  rpnnen2lem1  15851  sadadd2lem  16094  sadadd2  16095  pcmpt  16521  pcmptdvds  16523  prmreclem2  16546  prmreclem4  16548  prmreclem5  16549  prmreclem6  16550  prmrec  16551  ramub1lem2  16656  ramcl  16658  prmop1  16667  prmonn2  16668  prmdvdsprmo  16671  fvprmselelfz  16673  fvprmselgcd1  16674  prmodvdslcmf  16676  prmgapprmo  16691  smndex2dlinvh  18471  pmtrval  18974  pmtrdifellem3  19001  cyggenod2  19400  gsummpt1n0  19481  dmdprdsplitlem  19555  cycsubggenodd  19627  cyggic  20692  evlslem2  21199  coe1tmmul2fv  21359  coe1pwmulfv  21361  dmatmulcl  21557  scmatscmiddistr  21565  marrepval  21619  maducoeval  21696  maducoeval2  21697  minmar1val  21705  fclsval  23067  stdbdmetval  23576  stdbdxmet  23577  pcopt2  24092  cmetcaulem  24357  ovolicc2lem3  24588  ovolicc2lem4  24589  ovolicc2lem5  24590  mbfposb  24722  i1fres  24775  i1fposd  24777  mbfi1fseqlem2  24786  mbfi1fseq  24791  mbfi1flimlem  24792  mbfi1flim  24793  itg2splitlem  24818  itg2cnlem1  24831  itg2cn  24833  isibl  24835  isibl2  24836  iblitg  24838  dfitg  24839  cbvitg  24845  itgeq2  24847  itgvallem  24854  iblneg  24872  itgneg  24873  itgss3  24884  itgcn  24914  deg1suble  25177  elply2  25262  dgrsub  25338  aareccl  25391  vmaval  26167  prmorcht  26232  pclogsum  26268  dchrelbasd  26292  dchrptlem2  26318  bposlem5  26341  lgsfval  26355  lgsdir  26385  lgsdilem2  26386  lgsdi  26387  lgsne0  26388  rplogsumlem2  26538  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  ballotlemsval  32375  ballotlemieq  32383  mrsubfval  33370  ttrcltr  33702  poimirlem1  35705  poimirlem5  35709  poimirlem6  35710  poimirlem12  35716  poimirlem22  35726  mblfinlem2  35742  itg2addnclem  35755  ftc1anclem5  35781  ftc1anclem6  35782  cdlemk40  38858  fsuppind  40202  dvnprodlem1  43377  fourierdlem86  43623  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  isomennd  43959  hsphoif  44004  hsphoival  44007  sge0hsphoire  44017  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hoidmvlelem5  44027  hspval  44037  hoidifhspval2  44043  hoidifhspval3  44047  hspmbllem2  44055  afveq12d  44512