Theorem fvco3d 6986

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ∘ ccom 5667  ⟶wf 6536  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548

This theorem is used by:  opco1  8120  opco2  8121  suppcoss  8205  wemapwe  9669  canthp1lem2  10649  yonedainv  18355  frgpcyg  21753  rhmcomulmpl  22305  selvvvval  22323  psdmplcl  22355  comet  24701  dvcobr  26136  ofrco  33002  constcof  33013  gsumpart  33423  pmtrcnel  33449  elrgspnlem1  33602  mplasclco  33946  selvply1rhmlem2  33951  esplymhp  33998  esplyfv1  33999  esplyfv  34000  esplyfval3  34002  subfacp1lem5  35689  aks5lem3a  42989  rhmcomulpsr  43347  evlselv  43354  extoimad  44923  imo72b2lem0  44924  imo72b2lem1  44928  chnsubseq  47629  fcores  47837  fcoresf1lem  47838  grimco  48687  upgrimwlklem5  48699  upgrimpthslem2  48706  upgrimcycls  48709  uspgrlimlem3  48788  fuco111x  50142  fuco112xa  50144  fuco11idx  50146  fuco22natlem3  50155  fuco22natlem  50156  fucoid  50159  fucocolem4  50167  fucolid  50172  fucorid  50173  precofvallem  50177  prcof22a  50203