Theorem fvoveq1d 7173

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

Syntax hints:   → wi 4   = wceq 1539  ‘cfv 6336  (class class class)co 7151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-un 3864  df-in 3866  df-ss 3876  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-iota 6295  df-fv 6344  df-ov 7154

This theorem is referenced by:  fvoveq1  7174  imbrov2fvoveq  7176  hashfzp1  13835  pfxfvlsw  14097  swrdswrd  14107  revrev  14169  cshwidx0mod  14207  2cshw  14215  lswcshw  14217  cshweqrep  14223  cshimadifsn0  14232  lswco  14241  cau3lem  14755  clim  14892  rlim  14893  rlim2  14894  clim2  14902  rlimclim  14944  climrlim2  14945  climshftlem  14972  rlimcn2  14988  climcn2  14990  subcn2  14992  isercoll  15065  climcau  15068  caurcvg2  15075  caucvgb  15077  iseralt  15082  climcndslem1  15245  smumullem  15884  prmreclem4  16303  cshwsidrepsw  16478  efgredlem  18933  islmhm2  19871  coe1pwmul  20996  coe1sclmul  20999  evl1gsumadd  21070  chfacfscmulgsum  21553  chfacfpmmulgsum  21557  mulc1cncf  23599  pcovalg  23706  ehl1eudisval  24114  ovolunlem1a  24189  ovolunlem1  24190  mbfi1fseq  24414  isibl  24458  isibl2  24459  cbvitg  24468  itgeqa  24506  dveflem  24671  dvferm1lem  24676  dvferm1  24677  dvferm2lem  24678  dvferm2  24679  dvlip  24685  c1lip1  24689  lhop1lem  24705  lhop1  24706  ftc1lem5  24732  vieta1lem2  24999  aalioulem3  25022  ulmshftlem  25076  ulmcaulem  25081  ulmcau  25082  ulmdvlem3  25089  rlimcnp  25643  scvxcvx  25663  jensenlem2  25665  lgamgulmlem2  25707  lgamgulmlem5  25710  lgamgulm2  25713  lgamcvglem  25717  lgamcvg2  25732  basellem4  25761  basellem5  25762  pcbcctr  25952  dchrisumlem3  26167  dchrmusumlema  26169  dchrmusum2  26170  dchrvmasumlem2  26174  dchrvmasumlema  26176  dchrvmasumiflem1  26177  dchrisum0lema  26190  dchrisum0lem1b  26191  dchrisum0lem2  26194  dchrisum0  26196  chpdifbndlem1  26229  selbergsb  26251  pntlemo  26283  crctcshwlkn0lem2  27689  crctcshwlkn0lem3  27690  crctcshlem4  27698  crctcsh  27702  clwwisshclwwslemlem  27890  lnolin  28629  lnoadd  28633  norm3adifi  29028  lnopl  29789  lnfnl  29806  lnopaddi  29846  lnfnaddi  29918  pfxlsw2ccat  30741  lmatfval  31278  xrge0iifhom  31401  itgeq12dv  31805  signsply0  32042  revwlk  32595  snmlval  32802  iprodgam  33216  knoppcnlem1  34215  knoppndvlem21  34254  matunitlindflem1  35326  poimirlem29  35359  poimirlem32  35362  itg2addnclem3  35383  ftc1cnnc  35402  ftc1anclem6  35408  ftc1anclem7  35409  geomcau  35470  lfli  36630  lfladd  36635  docavalN  38692  diaocN  38694  dihjatc  38986  dvh4dimat  39007  irrapxlem3  40131  irrapxlem4  40132  pellexlem6  40141  rmxfval  40211  rmyfval  40212  hashnzfz  41390  hashnzfzclim  41392  climsuse  42609  mullimc  42617  climf  42623  mullimcf  42624  idlimc  42627  limcperiod  42629  clim2f  42637  limcleqr  42645  limclner  42652  climf2  42667  clim2f2  42671  fnlimabslt  42680  climuz  42745  fperdvper  42920  ioodvbdlimc1lem2  42933  ioodvbdlimc2lem  42935  dvnmul  42944  stoweidlem9  43010  wallispilem4  43069  wallispilem5  43070  dirkerval  43092  dirkerval2  43095  dirkertrigeqlem1  43099  dirkertrigeqlem2  43100  dirkertrigeq  43102  dirkercncflem2  43105  ovnhoi  43601  hspmbllem1  43624  digfval  45369  dignn0flhalflem2  45388