Theorem ifbieq1d 4530

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-un 3936  df-if 4506

This theorem is referenced by:  opeq1  4854  opeq2  4855  oieq1  9531  oieq2  9532  cantnflem1d  9707  cantnflem1  9708  ttrcltr  9735  iunfictbso  10133  ttukey2g  10535  bcval  14327  swrdval  14666  summolem2a  15736  zsum  15739  fsum  15741  sumss  15745  sumss2  15747  fsumcvg2  15748  fsumser  15751  isumless  15866  cbvprod  15934  cbvprodv  15935  prodmolem2a  15955  zprod  15958  fprod  15962  fprodntriv  15963  prodss  15968  rpnnen2lem1  16237  sadadd2lem  16483  sadadd2  16484  pcmpt  16917  pcmptdvds  16919  prmreclem2  16942  prmreclem4  16944  prmreclem5  16945  prmreclem6  16946  prmrec  16947  ramub1lem2  17052  ramcl  17054  prmop1  17063  prmonn2  17064  prmdvdsprmo  17067  fvprmselelfz  17069  fvprmselgcd1  17070  prmodvdslcmf  17072  prmgapprmo  17087  smndex2dlinvh  18900  pmtrval  19437  pmtrdifellem3  19464  cyggenod2  19871  gsummpt1n0  19951  dmdprdsplitlem  20025  cycsubggenodd  20097  cyggic  21538  evlslem2  22042  coe1tmmul2fv  22220  coe1pwmulfv  22222  dmatmulcl  22443  scmatscmiddistr  22451  marrepval  22505  maducoeval  22582  maducoeval2  22583  minmar1val  22591  fclsval  23951  stdbdmetval  24458  stdbdxmet  24459  pcopt2  24979  cmetcaulem  25245  ovolicc2lem3  25477  ovolicc2lem4  25478  ovolicc2lem5  25479  mbfposb  25611  i1fres  25663  i1fposd  25665  mbfi1fseqlem2  25674  mbfi1fseq  25679  mbfi1flimlem  25680  mbfi1flim  25681  itg2splitlem  25706  itg2cnlem1  25719  itg2cn  25721  isibl  25723  isibl2  25724  iblitg  25726  dfitg  25727  cbvitg  25734  itgeq2  25736  itgvallem  25743  iblneg  25761  itgneg  25762  itgss3  25773  itgcn  25803  deg1suble  26069  elply2  26158  dgrsub  26235  aareccl  26291  vmaval  27080  prmorcht  27145  pclogsum  27183  dchrelbasd  27207  dchrptlem2  27233  bposlem5  27256  lgsfval  27270  lgsdir  27300  lgsdilem2  27301  lgsdi  27302  lgsne0  27303  rplogsumlem2  27453  pntrlog2bndlem4  27548  pntrlog2bndlem5  27549  elrspunsn  33449  gsummoncoe1fzo  33612  fldextrspunlsp  33720  ballotlemsval  34546  ballotlemieq  34554  mrsubfval  35535  cbvprodvw2  36270  cbvproddavw  36303  cbvsumdavw2  36318  cbvproddavw2  36319  poimirlem1  37650  poimirlem5  37654  poimirlem6  37655  poimirlem12  37661  poimirlem22  37671  mblfinlem2  37687  itg2addnclem  37700  ftc1anclem5  37726  ftc1anclem6  37727  cdlemk40  40941  fsuppind  42588  cantnfub  43320  dvnprodlem1  45955  fourierdlem86  46201  fourierdlem97  46212  fourierdlem103  46218  fourierdlem104  46219  fourierdlem112  46227  isomennd  46540  hsphoif  46585  hsphoival  46588  sge0hsphoire  46598  hoidmv1lelem2  46601  hoidmv1lelem3  46602  hoidmv1le  46603  hoidmvlelem1  46604  hoidmvlelem2  46605  hoidmvlelem3  46606  hoidmvlelem4  46607  hoidmvlelem5  46608  hspval  46618  hoidifhspval2  46624  hoidifhspval3  46628  hspmbllem2  46636  afveq12d  47142  discsubc  49011  oppfvalg  49054