Theorem fvco3d 6934

Description: Value of a function composition. Deduction form of fvco3 6933. (Contributed by Stanislas Polu, 9-Mar-2020.)

Hypotheses

Ref	Expression
fvco3d.1	⊢ (𝜑 → 𝐺:𝐴⟶𝐵)
fvco3d.2	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
fvco3d	⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))

Proof of Theorem fvco3d

Step	Hyp	Ref	Expression
1		fvco3d.1	. 2 ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)
2		fvco3d.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
3		fvco3 6933	. 2 ⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ∘ ccom 5628  ⟶wf 6488  ‘cfv 6492

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  opco1  8066  opco2  8067  suppcoss  8150  wemapwe  9609  canthp1lem2  10567  yonedainv  18238  frgpcyg  21563  psdmplcl  22138  rhmcomulmpl  22357  comet  24488  dvcobr  25923  ofrco  32698  constcof  32709  gsumpart  33139  pmtrcnel  33165  elrgspnlem1  33318  esplymhp  33727  esplyfv1  33728  esplyfv  33729  esplyfval3  33731  subfacp1lem5  35382  aks5lem3a  42642  rhmcomulpsr  43008  selvvvval  43032  evlselv  43034  extoimad  44609  imo72b2lem0  44610  imo72b2lem1  44614  chnsubseq  47326  fcores  47527  fcoresf1lem  47528  grimco  48377  upgrimwlklem5  48389  upgrimpthslem2  48396  upgrimcycls  48399  uspgrlimlem3  48478  fuco111x  49818  fuco112xa  49820  fuco11idx  49822  fuco22natlem3  49831  fuco22natlem  49832  fucoid  49835  fucocolem4  49843  fucolid  49848  fucorid  49849  precofvallem  49853  prcof22a  49879