Theorem fvco3d 6928

Description: Value of a function composition. Deduction form of fvco3 6927. (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 6927	. 2 ⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))
4	1, 2, 3	syl2anc 590	1 ⊢ (𝜑 → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶)))

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ∘ ccom 5622  ⟶wf 6481  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-fv 6493

This theorem is referenced by:  opco1  8062  opco2  8063  suppcoss  8147  wemapwe  9609  canthp1lem2  10567  yonedainv  18238  frgpcyg  21548  rhmcomulmpl  22100  selvvvval  22118  psdmplcl  22150  comet  24496  dvcobr  25931  ofrco  32702  constcof  32713  gsumpart  33144  pmtrcnel  33170  elrgspnlem1  33323  mplasclco  33700  selvply1rhmlem2  33705  esplymhp  33752  esplyfv1  33753  esplyfv  33754  esplyfval3  33756  subfacp1lem5  35412  aks5lem3a  42674  rhmcomulpsr  43032  evlselv  43039  extoimad  44608  imo72b2lem0  44609  imo72b2lem1  44613  chnsubseq  47325  fcores  47530  fcoresf1lem  47531  grimco  48380  upgrimwlklem5  48392  upgrimpthslem2  48399  upgrimcycls  48402  uspgrlimlem3  48481  fuco111x  49821  fuco112xa  49823  fuco11idx  49825  fuco22natlem3  49834  fuco22natlem  49835  fucoid  49838  fucocolem4  49846  fucolid  49851  fucorid  49852  precofvallem  49856  prcof22a  49882