Theorem fvoveq1d 7427

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

Syntax hints:   → wi 4   = wceq 1541  ‘cfv 6540  (class class class)co 7405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408

This theorem is referenced by:  fvoveq1  7428  imbrov2fvoveq  7430  hashfzp1  14387  pfxfvlsw  14641  swrdswrd  14651  revrev  14713  cshwidx0mod  14751  2cshw  14759  lswcshw  14761  cshweqrep  14767  cshimadifsn0  14777  lswco  14786  cau3lem  15297  clim  15434  rlim  15435  rlim2  15436  clim2  15444  rlimclim  15486  climrlim2  15487  climshftlem  15514  rlimcn3  15530  climcn2  15533  subcn2  15535  isercoll  15610  climcau  15613  caurcvg2  15620  caucvgb  15622  iseralt  15627  climcndslem1  15791  smumullem  16429  prmreclem4  16848  cshwsidrepsw  17023  efgredlem  19609  islmhm2  20641  coe1pwmul  21792  coe1sclmul  21795  evl1gsumadd  21868  chfacfscmulgsum  22353  chfacfpmmulgsum  22357  mulc1cncf  24412  pcovalg  24519  ehl1eudisval  24929  ovolunlem1a  25004  ovolunlem1  25005  mbfi1fseq  25230  isibl  25274  isibl2  25275  cbvitg  25284  itgeqa  25322  dveflem  25487  dvferm1lem  25492  dvferm1  25493  dvferm2lem  25494  dvferm2  25495  dvlip  25501  c1lip1  25505  lhop1lem  25521  lhop1  25522  ftc1lem5  25548  vieta1lem2  25815  aalioulem3  25838  ulmshftlem  25892  ulmcaulem  25897  ulmcau  25898  ulmdvlem3  25905  rlimcnp  26459  scvxcvx  26479  jensenlem2  26481  lgamgulmlem2  26523  lgamgulmlem5  26526  lgamgulm2  26529  lgamcvglem  26533  lgamcvg2  26548  basellem4  26577  basellem5  26578  pcbcctr  26768  dchrisumlem3  26983  dchrmusumlema  26985  dchrmusum2  26986  dchrvmasumlem2  26990  dchrvmasumlema  26992  dchrvmasumiflem1  26993  dchrisum0lema  27006  dchrisum0lem1b  27007  dchrisum0lem2  27010  dchrisum0  27012  chpdifbndlem1  27045  selbergsb  27067  pntlemo  27099  crctcshwlkn0lem2  29054  crctcshwlkn0lem3  29055  crctcshlem4  29063  crctcsh  29067  clwwisshclwwslemlem  29255  lnolin  29994  lnoadd  29998  norm3adifi  30393  lnopl  31154  lnfnl  31171  lnopaddi  31211  lnfnaddi  31283  pfxlsw2ccat  32103  lmatfval  32782  xrge0iifhom  32905  itgeq12dv  33313  signsply0  33550  revwlk  34103  snmlval  34310  iprodgam  34700  mpomulcn  35150  knoppcnlem1  35357  knoppndvlem21  35396  matunitlindflem1  36472  poimirlem29  36505  poimirlem32  36508  itg2addnclem3  36529  ftc1cnnc  36548  ftc1anclem6  36554  ftc1anclem7  36555  geomcau  36615  lfli  37919  lfladd  37924  docavalN  39982  diaocN  39984  dihjatc  40276  dvh4dimat  40297  sticksstones10  40959  sticksstones12a  40961  irrapxlem3  41547  irrapxlem4  41548  pellexlem6  41557  rmxfval  41627  rmyfval  41628  hashnzfz  43064  hashnzfzclim  43066  caucvgbf  44186  cvgcaule  44188  climsuse  44310  mullimc  44318  climf  44324  mullimcf  44325  idlimc  44328  limcperiod  44330  clim2f  44338  limcleqr  44346  limclner  44353  climf2  44368  clim2f2  44372  fnlimabslt  44381  climuz  44446  fperdvper  44621  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  dvnmul  44645  stoweidlem9  44711  wallispilem4  44770  wallispilem5  44771  dirkerval  44793  dirkerval2  44796  dirkertrigeqlem1  44800  dirkertrigeqlem2  44801  dirkertrigeq  44803  dirkercncflem2  44806  ovnhoi  45305  hspmbllem1  45328  digfval  47236  dignn0flhalflem2  47255