Theorem ifbieq1d 4515

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ifcif 4491

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-un 3918  df-if 4492

This theorem is referenced by:  opeq1  4835  opeq2  4836  oieq1  9457  oieq2  9458  cantnflem1d  9633  cantnflem1  9634  ttrcltr  9661  iunfictbso  10059  ttukey2g  10461  bcval  14214  swrdval  14543  summolem2a  15611  zsum  15614  fsum  15616  sumss  15620  sumss2  15622  fsumcvg2  15623  fsumser  15626  isumless  15741  cbvprod  15809  prodmolem2a  15828  zprod  15831  fprod  15835  fprodntriv  15836  prodss  15841  rpnnen2lem1  16107  sadadd2lem  16350  sadadd2  16351  pcmpt  16775  pcmptdvds  16777  prmreclem2  16800  prmreclem4  16802  prmreclem5  16803  prmreclem6  16804  prmrec  16805  ramub1lem2  16910  ramcl  16912  prmop1  16921  prmonn2  16922  prmdvdsprmo  16925  fvprmselelfz  16927  fvprmselgcd1  16928  prmodvdslcmf  16930  prmgapprmo  16945  smndex2dlinvh  18741  pmtrval  19247  pmtrdifellem3  19274  cyggenod2  19676  gsummpt1n0  19756  dmdprdsplitlem  19830  cycsubggenodd  19902  cyggic  21016  evlslem2  21526  coe1tmmul2fv  21686  coe1pwmulfv  21688  dmatmulcl  21886  scmatscmiddistr  21894  marrepval  21948  maducoeval  22025  maducoeval2  22026  minmar1val  22034  fclsval  23396  stdbdmetval  23907  stdbdxmet  23908  pcopt2  24423  cmetcaulem  24689  ovolicc2lem3  24920  ovolicc2lem4  24921  ovolicc2lem5  24922  mbfposb  25054  i1fres  25107  i1fposd  25109  mbfi1fseqlem2  25118  mbfi1fseq  25123  mbfi1flimlem  25124  mbfi1flim  25125  itg2splitlem  25150  itg2cnlem1  25163  itg2cn  25165  isibl  25167  isibl2  25168  iblitg  25170  dfitg  25171  cbvitg  25177  itgeq2  25179  itgvallem  25186  iblneg  25204  itgneg  25205  itgss3  25216  itgcn  25246  deg1suble  25509  elply2  25594  dgrsub  25670  aareccl  25723  vmaval  26499  prmorcht  26564  pclogsum  26600  dchrelbasd  26624  dchrptlem2  26650  bposlem5  26673  lgsfval  26687  lgsdir  26717  lgsdilem2  26718  lgsdi  26719  lgsne0  26720  rplogsumlem2  26870  pntrlog2bndlem4  26965  pntrlog2bndlem5  26966  gsummoncoe1fzo  32367  ballotlemsval  33197  ballotlemieq  33205  mrsubfval  34189  poimirlem1  36152  poimirlem5  36156  poimirlem6  36157  poimirlem12  36163  poimirlem22  36173  mblfinlem2  36189  itg2addnclem  36202  ftc1anclem5  36228  ftc1anclem6  36229  cdlemk40  39453  fsuppind  40823  cantnfub  41714  dvnprodlem1  44307  fourierdlem86  44553  fourierdlem97  44564  fourierdlem103  44570  fourierdlem104  44571  fourierdlem112  44579  isomennd  44892  hsphoif  44937  hsphoival  44940  sge0hsphoire  44950  hoidmv1lelem2  44953  hoidmv1lelem3  44954  hoidmv1le  44955  hoidmvlelem1  44956  hoidmvlelem2  44957  hoidmvlelem3  44958  hoidmvlelem4  44959  hoidmvlelem5  44960  hspval  44970  hoidifhspval2  44976  hoidifhspval3  44980  hspmbllem2  44988  afveq12d  45485