Theorem fvoveq1d 7412

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

Syntax hints:   → wi 4   = wceq 1540  ‘cfv 6514  (class class class)co 7390

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  fvoveq1  7413  imbrov2fvoveq  7415  hashfzp1  14403  pfxfvlsw  14667  swrdswrd  14677  revrev  14739  cshwidx0mod  14777  2cshw  14785  lswcshw  14787  cshweqrep  14793  cshimadifsn0  14803  lswco  14812  cau3lem  15328  clim  15467  rlim  15468  rlim2  15469  clim2  15477  rlimclim  15519  climrlim2  15520  climshftlem  15547  rlimcn3  15563  climcn2  15566  subcn2  15568  isercoll  15641  climcau  15644  caurcvg2  15651  caucvgb  15653  iseralt  15658  climcndslem1  15822  smumullem  16469  prmreclem4  16897  cshwsidrepsw  17071  efgredlem  19684  islmhm2  20952  coe1pwmul  22172  coe1sclmul  22175  evl1gsumadd  22252  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  mpomulcn  24765  mulc1cncf  24805  pcovalg  24919  ehl1eudisval  25328  ovolunlem1a  25404  ovolunlem1  25405  mbfi1fseq  25629  isibl  25673  isibl2  25674  cbvitg  25684  cbvitgv  25685  itgeqa  25722  dveflem  25890  dvferm1lem  25895  dvferm1  25896  dvferm2lem  25897  dvferm2  25898  dvlip  25905  c1lip1  25909  lhop1lem  25925  lhop1  25926  ftc1lem5  25954  vieta1lem2  26226  aalioulem3  26249  ulmshftlem  26305  ulmcaulem  26310  ulmcau  26311  ulmdvlem3  26318  rlimcnp  26882  scvxcvx  26903  jensenlem2  26905  lgamgulmlem2  26947  lgamgulmlem5  26950  lgamgulm2  26953  lgamcvglem  26957  lgamcvg2  26972  basellem4  27001  basellem5  27002  pcbcctr  27194  dchrisumlem3  27409  dchrmusumlema  27411  dchrmusum2  27412  dchrvmasumlem2  27416  dchrvmasumlema  27418  dchrvmasumiflem1  27419  dchrisum0lema  27432  dchrisum0lem1b  27433  dchrisum0lem2  27436  dchrisum0  27438  chpdifbndlem1  27471  selbergsb  27493  pntlemo  27525  crctcshwlkn0lem2  29748  crctcshwlkn0lem3  29749  crctcshlem4  29757  crctcsh  29761  clwwisshclwwslemlem  29949  lnolin  30690  lnoadd  30694  norm3adifi  31089  lnopl  31850  lnfnl  31867  lnopaddi  31907  lnfnaddi  31979  pfxlsw2ccat  32879  constrrtlc1  33729  constrrtcc  33732  lmatfval  33811  xrge0iifhom  33934  itgeq12dv  34324  signsply0  34549  revwlk  35119  snmlval  35325  iprodgam  35736  cbvitgvw2  36243  cbvitgdavw  36276  cbvitgdavw2  36292  knoppcnlem1  36488  knoppndvlem21  36527  matunitlindflem1  37617  poimirlem29  37650  poimirlem32  37653  itg2addnclem3  37674  ftc1cnnc  37693  ftc1anclem6  37699  ftc1anclem7  37700  geomcau  37760  lfli  39061  lfladd  39066  docavalN  41124  diaocN  41126  dihjatc  41418  dvh4dimat  41439  sticksstones10  42150  sticksstones12a  42152  irrapxlem3  42819  irrapxlem4  42820  pellexlem6  42829  rmxfval  42899  rmyfval  42900  hashnzfz  44316  hashnzfzclim  44318  caucvgbf  45492  cvgcaule  45494  climsuse  45613  mullimc  45621  climf  45627  mullimcf  45628  idlimc  45631  limcperiod  45633  clim2f  45641  limcleqr  45649  limclner  45656  climf2  45671  clim2f2  45675  fnlimabslt  45684  climuz  45749  fperdvper  45924  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnmul  45948  stoweidlem9  46014  wallispilem4  46073  wallispilem5  46074  dirkerval  46096  dirkerval2  46099  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkertrigeq  46106  dirkercncflem2  46109  ovnhoi  46608  hspmbllem1  46631  digfval  48590  dignn0flhalflem2  48609  dfinito4  49494  ranfval  49607