Theorem fvoveq1d 7453

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 7446	. 2 ⊢ (𝜑 → (𝐴𝑂𝐶) = (𝐵𝑂𝐶))
3	2	fveq2d 6910	1 ⊢ (𝜑 → (𝐹‘(𝐴𝑂𝐶)) = (𝐹‘(𝐵𝑂𝐶)))

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6561  (class class class)co 7431

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  fvoveq1  7454  imbrov2fvoveq  7456  hashfzp1  14470  pfxfvlsw  14733  swrdswrd  14743  revrev  14805  cshwidx0mod  14843  2cshw  14851  lswcshw  14853  cshweqrep  14859  cshimadifsn0  14869  lswco  14878  cau3lem  15393  clim  15530  rlim  15531  rlim2  15532  clim2  15540  rlimclim  15582  climrlim2  15583  climshftlem  15610  rlimcn3  15626  climcn2  15629  subcn2  15631  isercoll  15704  climcau  15707  caurcvg2  15714  caucvgb  15716  iseralt  15721  climcndslem1  15885  smumullem  16529  prmreclem4  16957  cshwsidrepsw  17131  efgredlem  19765  islmhm2  21037  coe1pwmul  22282  coe1sclmul  22285  evl1gsumadd  22362  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  mpomulcn  24891  mulc1cncf  24931  pcovalg  25045  ehl1eudisval  25455  ovolunlem1a  25531  ovolunlem1  25532  mbfi1fseq  25756  isibl  25800  isibl2  25801  cbvitg  25811  cbvitgv  25812  itgeqa  25849  dveflem  26017  dvferm1lem  26022  dvferm1  26023  dvferm2lem  26024  dvferm2  26025  dvlip  26032  c1lip1  26036  lhop1lem  26052  lhop1  26053  ftc1lem5  26081  vieta1lem2  26353  aalioulem3  26376  ulmshftlem  26432  ulmcaulem  26437  ulmcau  26438  ulmdvlem3  26445  rlimcnp  27008  scvxcvx  27029  jensenlem2  27031  lgamgulmlem2  27073  lgamgulmlem5  27076  lgamgulm2  27079  lgamcvglem  27083  lgamcvg2  27098  basellem4  27127  basellem5  27128  pcbcctr  27320  dchrisumlem3  27535  dchrmusumlema  27537  dchrmusum2  27538  dchrvmasumlem2  27542  dchrvmasumlema  27544  dchrvmasumiflem1  27545  dchrisum0lema  27558  dchrisum0lem1b  27559  dchrisum0lem2  27562  dchrisum0  27564  chpdifbndlem1  27597  selbergsb  27619  pntlemo  27651  crctcshwlkn0lem2  29831  crctcshwlkn0lem3  29832  crctcshlem4  29840  crctcsh  29844  clwwisshclwwslemlem  30032  lnolin  30773  lnoadd  30777  norm3adifi  31172  lnopl  31933  lnfnl  31950  lnopaddi  31990  lnfnaddi  32062  pfxlsw2ccat  32935  constrrtlc1  33773  constrrtcc  33776  lmatfval  33813  xrge0iifhom  33936  itgeq12dv  34328  signsply0  34566  revwlk  35130  snmlval  35336  iprodgam  35742  cbvitgvw2  36249  cbvitgdavw  36282  cbvitgdavw2  36298  knoppcnlem1  36494  knoppndvlem21  36533  matunitlindflem1  37623  poimirlem29  37656  poimirlem32  37659  itg2addnclem3  37680  ftc1cnnc  37699  ftc1anclem6  37705  ftc1anclem7  37706  geomcau  37766  lfli  39062  lfladd  39067  docavalN  41125  diaocN  41127  dihjatc  41419  dvh4dimat  41440  sticksstones10  42156  sticksstones12a  42158  irrapxlem3  42835  irrapxlem4  42836  pellexlem6  42845  rmxfval  42915  rmyfval  42916  hashnzfz  44339  hashnzfzclim  44341  caucvgbf  45500  cvgcaule  45502  climsuse  45623  mullimc  45631  climf  45637  mullimcf  45638  idlimc  45641  limcperiod  45643  clim2f  45651  limcleqr  45659  limclner  45666  climf2  45681  clim2f2  45685  fnlimabslt  45694  climuz  45759  fperdvper  45934  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnmul  45958  stoweidlem9  46024  wallispilem4  46083  wallispilem5  46084  dirkerval  46106  dirkerval2  46109  dirkertrigeqlem1  46113  dirkertrigeqlem2  46114  dirkertrigeq  46116  dirkercncflem2  46119  ovnhoi  46618  hspmbllem1  46641  digfval  48518  dignn0flhalflem2  48537