Theorem fvoveq1d 7470

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

Syntax hints:   → wi 4   = wceq 1537  ‘cfv 6573  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  fvoveq1  7471  imbrov2fvoveq  7473  hashfzp1  14480  pfxfvlsw  14743  swrdswrd  14753  revrev  14815  cshwidx0mod  14853  2cshw  14861  lswcshw  14863  cshweqrep  14869  cshimadifsn0  14879  lswco  14888  cau3lem  15403  clim  15540  rlim  15541  rlim2  15542  clim2  15550  rlimclim  15592  climrlim2  15593  climshftlem  15620  rlimcn3  15636  climcn2  15639  subcn2  15641  isercoll  15716  climcau  15719  caurcvg2  15726  caucvgb  15728  iseralt  15733  climcndslem1  15897  smumullem  16538  prmreclem4  16966  cshwsidrepsw  17141  efgredlem  19789  islmhm2  21060  coe1pwmul  22303  coe1sclmul  22306  evl1gsumadd  22383  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  mpomulcn  24910  mulc1cncf  24950  pcovalg  25064  ehl1eudisval  25474  ovolunlem1a  25550  ovolunlem1  25551  mbfi1fseq  25776  isibl  25820  isibl2  25821  cbvitg  25831  cbvitgv  25832  itgeqa  25869  dveflem  26037  dvferm1lem  26042  dvferm1  26043  dvferm2lem  26044  dvferm2  26045  dvlip  26052  c1lip1  26056  lhop1lem  26072  lhop1  26073  ftc1lem5  26101  vieta1lem2  26371  aalioulem3  26394  ulmshftlem  26450  ulmcaulem  26455  ulmcau  26456  ulmdvlem3  26463  rlimcnp  27026  scvxcvx  27047  jensenlem2  27049  lgamgulmlem2  27091  lgamgulmlem5  27094  lgamgulm2  27097  lgamcvglem  27101  lgamcvg2  27116  basellem4  27145  basellem5  27146  pcbcctr  27338  dchrisumlem3  27553  dchrmusumlema  27555  dchrmusum2  27556  dchrvmasumlem2  27560  dchrvmasumlema  27562  dchrvmasumiflem1  27563  dchrisum0lema  27576  dchrisum0lem1b  27577  dchrisum0lem2  27580  dchrisum0  27582  chpdifbndlem1  27615  selbergsb  27637  pntlemo  27669  crctcshwlkn0lem2  29844  crctcshwlkn0lem3  29845  crctcshlem4  29853  crctcsh  29857  clwwisshclwwslemlem  30045  lnolin  30786  lnoadd  30790  norm3adifi  31185  lnopl  31946  lnfnl  31963  lnopaddi  32003  lnfnaddi  32075  pfxlsw2ccat  32917  constrrtlc1  33723  constrrtcc  33726  lmatfval  33760  xrge0iifhom  33883  itgeq12dv  34291  signsply0  34528  revwlk  35092  snmlval  35299  iprodgam  35704  cbvitgvw2  36214  cbvitgdavw  36247  cbvitgdavw2  36263  knoppcnlem1  36459  knoppndvlem21  36498  matunitlindflem1  37576  poimirlem29  37609  poimirlem32  37612  itg2addnclem3  37633  ftc1cnnc  37652  ftc1anclem6  37658  ftc1anclem7  37659  geomcau  37719  lfli  39017  lfladd  39022  docavalN  41080  diaocN  41082  dihjatc  41374  dvh4dimat  41395  sticksstones10  42112  sticksstones12a  42114  irrapxlem3  42780  irrapxlem4  42781  pellexlem6  42790  rmxfval  42860  rmyfval  42861  hashnzfz  44289  hashnzfzclim  44291  caucvgbf  45405  cvgcaule  45407  climsuse  45529  mullimc  45537  climf  45543  mullimcf  45544  idlimc  45547  limcperiod  45549  clim2f  45557  limcleqr  45565  limclner  45572  climf2  45587  clim2f2  45591  fnlimabslt  45600  climuz  45665  fperdvper  45840  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmul  45864  stoweidlem9  45930  wallispilem4  45989  wallispilem5  45990  dirkerval  46012  dirkerval2  46015  dirkertrigeqlem1  46019  dirkertrigeqlem2  46020  dirkertrigeq  46022  dirkercncflem2  46025  ovnhoi  46524  hspmbllem1  46547  digfval  48331  dignn0flhalflem2  48350