Theorem fvoveq1d 7433

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

Syntax hints:   → wi 4   = wceq 1567  ‘cfv 6537  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  fvoveq1  7434  imbrov2fvoveq  7436  hashfzp1  14467  pfxfvlsw  14731  swrdswrd  14741  revrev  14803  cshwidx0mod  14841  2cshw  14849  lswcshw  14851  cshweqrep  14857  cshimadifsn0  14866  lswco  14875  cau3lem  15405  clim  15544  rlim  15545  rlim2  15546  clim2  15554  rlimclim  15596  climrlim2  15597  climshftlem  15624  rlimcn3  15640  climcn2  15643  subcn2  15645  isercoll  15718  climcau  15721  caurcvg2  15728  caucvgb  15730  iseralt  15735  climcndslem1  15902  smumullem  16549  prmreclem4  16978  cshwsidrepsw  17152  efgredlem  19816  islmhm2  21136  coe1pwmul  22408  coe1sclmul  22411  evl1gsumadd  22486  chfacfscmulgsum  22985  chfacfpmmulgsum  22989  mpomulcn  24994  mulc1cncf  25032  pcovalg  25139  ehl1eudisval  25548  ovolunlem1a  25623  ovolunlem1  25624  mbfi1fseq  25848  isibl  25892  isibl2  25893  cbvitg  25903  cbvitgv  25904  itgeqa  25941  dveflem  26106  dvferm1lem  26111  dvferm1  26112  dvferm2lem  26113  dvferm2  26114  dvlip  26120  c1lip1  26124  lhop1lem  26140  lhop1  26141  ftc1lem5  26167  vieta1lem2  26440  aalioulem3  26463  ulmshftlem  26517  ulmcaulem  26522  ulmcau  26523  ulmdvlem3  26530  rlimcnp  27095  scvxcvx  27115  jensenlem2  27117  lgamgulmlem2  27159  lgamgulmlem5  27162  lgamgulm2  27165  lgamcvglem  27169  lgamcvg2  27184  basellem4  27213  basellem5  27214  pcbcctr  27405  dchrisumlem3  27620  dchrmusumlema  27622  dchrmusum2  27623  dchrvmasumlem2  27627  dchrvmasumlema  27629  dchrvmasumiflem1  27630  dchrisum0lema  27643  dchrisum0lem1b  27644  dchrisum0lem2  27647  dchrisum0  27649  chpdifbndlem1  27682  selbergsb  27704  pntlemo  27736  crctcshwlkn0lem2  30100  crctcshwlkn0lem3  30101  crctcshlem4  30109  crctcsh  30113  clwwisshclwwslemlem  30304  lnolin  31046  lnoadd  31050  norm3adifi  31445  lnopl  32206  lnfnl  32223  lnopaddi  32263  lnfnaddi  32335  pfxlsw2ccat  33210  extvfval  33866  mplvrpmrhm  33881  constrrtlc1  34066  constrrtcc  34069  lmatfval  34148  xrge0iifhom  34271  itgeq12dv  34660  signsply0  34882  revwlk  35515  snmlval  35721  iprodgam  36132  cbvitgvw2  36648  cbvitgdavw  36681  cbvitgdavw2  36697  knoppcnlem1  36970  knoppndvlem21  37009  matunitlindflem1  38154  poimirlem29  38187  poimirlem32  38190  itg2addnclem3  38211  ftc1cnnc  38230  ftc1anclem6  38236  ftc1anclem7  38237  geomcau  38297  lfli  39724  lfladd  39729  docavalN  41786  diaocN  41788  dihjatc  42080  dvh4dimat  42101  sticksstones10  42811  sticksstones12a  42813  irrapxlem3  43442  irrapxlem4  43443  pellexlem6  43452  rmxfval  43522  rmyfval  43523  hashnzfz  44921  hashnzfzclim  44923  caucvgbf  46094  cvgcaule  46096  climsuse  46215  mullimc  46223  climf  46229  mullimcf  46230  idlimc  46233  limcperiod  46235  clim2f  46241  limcleqr  46249  limclner  46256  climf2  46271  clim2f2  46275  fnlimabslt  46284  climuz  46349  fperdvper  46524  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  dvnmul  46548  stoweidlem9  46614  wallispilem4  46673  wallispilem5  46674  dirkerval  46696  dirkerval2  46699  dirkertrigeqlem1  46703  dirkertrigeqlem2  46704  dirkertrigeq  46706  dirkercncflem2  46709  fourierdlem48  46759  fourierdlem49  46760  fourierdlem113  46824  ovnhoi  47208  hspmbllem1  47231  digfval  49261  dignn0flhalflem2  49280  dfinito4  50163  ranfval  50276