Theorem fvoveq1d 7421

Description: Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.)

Hypothesis

Ref	Expression
fvoveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
fvoveq1d	⊢ (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Proof of Theorem fvoveq1d

Step	Hyp	Ref	Expression
1		fvoveq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	oveq1d 7414	. 2 ⊢ (𝜑 → (𝐴𝑂𝐶) = (𝐵𝑂𝐶))
3	2	fveq2d 6876	1 ⊢ (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1539  ‘cfv 6527  (class class class)co 7399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-iota 6480  df-fv 6535  df-ov 7402

This theorem is referenced by:  fvoveq1  7422  imbrov2fvoveq  7424  hashfzp1  14437  pfxfvlsw  14700  swrdswrd  14710  revrev  14772  cshwidx0mod  14810  2cshw  14818  lswcshw  14820  cshweqrep  14826  cshimadifsn0  14836  lswco  14845  cau3lem  15360  clim  15497  rlim  15498  rlim2  15499  clim2  15507  rlimclim  15549  climrlim2  15550  climshftlem  15577  rlimcn3  15593  climcn2  15596  subcn2  15598  isercoll  15671  climcau  15674  caurcvg2  15681  caucvgb  15683  iseralt  15688  climcndslem1  15852  smumullem  16496  prmreclem4  16924  cshwsidrepsw  17098  efgredlem  19713  islmhm2  20981  coe1pwmul  22201  coe1sclmul  22204  evl1gsumadd  22281  chfacfscmulgsum  22783  chfacfpmmulgsum  22787  mpomulcn  24794  mulc1cncf  24834  pcovalg  24948  ehl1eudisval  25358  ovolunlem1a  25434  ovolunlem1  25435  mbfi1fseq  25659  isibl  25703  isibl2  25704  cbvitg  25714  cbvitgv  25715  itgeqa  25752  dveflem  25920  dvferm1lem  25925  dvferm1  25926  dvferm2lem  25927  dvferm2  25928  dvlip  25935  c1lip1  25939  lhop1lem  25955  lhop1  25956  ftc1lem5  25984  vieta1lem2  26256  aalioulem3  26279  ulmshftlem  26335  ulmcaulem  26340  ulmcau  26341  ulmdvlem3  26348  rlimcnp  26911  scvxcvx  26932  jensenlem2  26934  lgamgulmlem2  26976  lgamgulmlem5  26979  lgamgulm2  26982  lgamcvglem  26986  lgamcvg2  27001  basellem4  27030  basellem5  27031  pcbcctr  27223  dchrisumlem3  27438  dchrmusumlema  27440  dchrmusum2  27441  dchrvmasumlem2  27445  dchrvmasumlema  27447  dchrvmasumiflem1  27448  dchrisum0lema  27461  dchrisum0lem1b  27462  dchrisum0lem2  27465  dchrisum0  27467  chpdifbndlem1  27500  selbergsb  27522  pntlemo  27554  crctcshwlkn0lem2  29725  crctcshwlkn0lem3  29726  crctcshlem4  29734  crctcsh  29738  clwwisshclwwslemlem  29926  lnolin  30667  lnoadd  30671  norm3adifi  31066  lnopl  31827  lnfnl  31844  lnopaddi  31884  lnfnaddi  31956  pfxlsw2ccat  32845  constrrtlc1  33682  constrrtcc  33685  lmatfval  33753  xrge0iifhom  33876  itgeq12dv  34266  signsply0  34504  revwlk  35068  snmlval  35274  iprodgam  35680  cbvitgvw2  36187  cbvitgdavw  36220  cbvitgdavw2  36236  knoppcnlem1  36432  knoppndvlem21  36471  matunitlindflem1  37561  poimirlem29  37594  poimirlem32  37597  itg2addnclem3  37618  ftc1cnnc  37637  ftc1anclem6  37643  ftc1anclem7  37644  geomcau  37704  lfli  39000  lfladd  39005  docavalN  41063  diaocN  41065  dihjatc  41357  dvh4dimat  41378  sticksstones10  42090  sticksstones12a  42092  irrapxlem3  42772  irrapxlem4  42773  pellexlem6  42782  rmxfval  42852  rmyfval  42853  hashnzfz  44270  hashnzfzclim  44272  caucvgbf  45444  cvgcaule  45446  climsuse  45567  mullimc  45575  climf  45581  mullimcf  45582  idlimc  45585  limcperiod  45587  clim2f  45595  limcleqr  45603  limclner  45610  climf2  45625  clim2f2  45629  fnlimabslt  45638  climuz  45703  fperdvper  45878  ioodvbdlimc1lem2  45891  ioodvbdlimc2lem  45893  dvnmul  45902  stoweidlem9  45968  wallispilem4  46027  wallispilem5  46028  dirkerval  46050  dirkerval2  46053  dirkertrigeqlem1  46057  dirkertrigeqlem2  46058  dirkertrigeq  46060  dirkercncflem2  46063  ovnhoi  46562  hspmbllem1  46585  digfval  48463  dignn0flhalflem2  48482  dfinito4  49171