Theorem fvoveq1d 7423

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

Syntax hints:   → wi 4   = wceq 1533  ‘cfv 6533  (class class class)co 7401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-iota 6485  df-fv 6541  df-ov 7404

This theorem is referenced by:  fvoveq1  7424  imbrov2fvoveq  7426  hashfzp1  14388  pfxfvlsw  14642  swrdswrd  14652  revrev  14714  cshwidx0mod  14752  2cshw  14760  lswcshw  14762  cshweqrep  14768  cshimadifsn0  14778  lswco  14787  cau3lem  15298  clim  15435  rlim  15436  rlim2  15437  clim2  15445  rlimclim  15487  climrlim2  15488  climshftlem  15515  rlimcn3  15531  climcn2  15534  subcn2  15536  isercoll  15611  climcau  15614  caurcvg2  15621  caucvgb  15623  iseralt  15628  climcndslem1  15792  smumullem  16430  prmreclem4  16851  cshwsidrepsw  17026  efgredlem  19657  islmhm2  20876  coe1pwmul  22120  coe1sclmul  22123  evl1gsumadd  22199  chfacfscmulgsum  22684  chfacfpmmulgsum  22688  mpomulcn  24707  mulc1cncf  24747  pcovalg  24861  ehl1eudisval  25271  ovolunlem1a  25347  ovolunlem1  25348  mbfi1fseq  25573  isibl  25617  isibl2  25618  cbvitg  25627  itgeqa  25665  dveflem  25833  dvferm1lem  25838  dvferm1  25839  dvferm2lem  25840  dvferm2  25841  dvlip  25848  c1lip1  25852  lhop1lem  25868  lhop1  25869  ftc1lem5  25897  vieta1lem2  26165  aalioulem3  26188  ulmshftlem  26242  ulmcaulem  26247  ulmcau  26248  ulmdvlem3  26255  rlimcnp  26813  scvxcvx  26834  jensenlem2  26836  lgamgulmlem2  26878  lgamgulmlem5  26881  lgamgulm2  26884  lgamcvglem  26888  lgamcvg2  26903  basellem4  26932  basellem5  26933  pcbcctr  27125  dchrisumlem3  27340  dchrmusumlema  27342  dchrmusum2  27343  dchrvmasumlem2  27347  dchrvmasumlema  27349  dchrvmasumiflem1  27350  dchrisum0lema  27363  dchrisum0lem1b  27364  dchrisum0lem2  27367  dchrisum0  27369  chpdifbndlem1  27402  selbergsb  27424  pntlemo  27456  crctcshwlkn0lem2  29534  crctcshwlkn0lem3  29535  crctcshlem4  29543  crctcsh  29547  clwwisshclwwslemlem  29735  lnolin  30476  lnoadd  30480  norm3adifi  30875  lnopl  31636  lnfnl  31653  lnopaddi  31693  lnfnaddi  31765  pfxlsw2ccat  32583  lmatfval  33283  xrge0iifhom  33406  itgeq12dv  33814  signsply0  34051  revwlk  34604  snmlval  34811  iprodgam  35207  knoppcnlem1  35859  knoppndvlem21  35898  matunitlindflem1  36974  poimirlem29  37007  poimirlem32  37010  itg2addnclem3  37031  ftc1cnnc  37050  ftc1anclem6  37056  ftc1anclem7  37057  geomcau  37117  lfli  38421  lfladd  38426  docavalN  40484  diaocN  40486  dihjatc  40778  dvh4dimat  40799  sticksstones10  41464  sticksstones12a  41466  irrapxlem3  42051  irrapxlem4  42052  pellexlem6  42061  rmxfval  42131  rmyfval  42132  hashnzfz  43568  hashnzfzclim  43570  caucvgbf  44685  cvgcaule  44687  climsuse  44809  mullimc  44817  climf  44823  mullimcf  44824  idlimc  44827  limcperiod  44829  clim2f  44837  limcleqr  44845  limclner  44852  climf2  44867  clim2f2  44871  fnlimabslt  44880  climuz  44945  fperdvper  45120  ioodvbdlimc1lem2  45133  ioodvbdlimc2lem  45135  dvnmul  45144  stoweidlem9  45210  wallispilem4  45269  wallispilem5  45270  dirkerval  45292  dirkerval2  45295  dirkertrigeqlem1  45299  dirkertrigeqlem2  45300  dirkertrigeq  45302  dirkercncflem2  45305  ovnhoi  45804  hspmbllem1  45827  digfval  47471  dignn0flhalflem2  47490