Theorem fvco3d 6961

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ∘ ccom 5642  ⟶wf 6507  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519

This theorem is referenced by:  opco1  8102  opco2  8103  suppcoss  8186  wemapwe  9650  canthp1lem2  10606  yonedainv  18242  frgpcyg  21483  psdmplcl  22049  rhmcomulmpl  22269  comet  24401  dvcobr  25849  gsumpart  32997  pmtrcnel  33046  elrgspnlem1  33193  subfacp1lem5  35171  aks5lem3a  42177  rhmcomulpsr  42539  selvvvval  42573  evlselv  42575  extoimad  44153  imo72b2lem0  44154  imo72b2lem1  44158  fcores  47068  fcoresf1lem  47069  grimco  47889  upgrimwlklem5  47901  upgrimpthslem2  47908  upgrimcycls  47911  uspgrlimlem3  47989  fuco111x  49320  fuco112xa  49322  fuco11idx  49324  fuco22natlem3  49333  fuco22natlem  49334  fucoid  49337  fucocolem4  49345  fucolid  49350  fucorid  49351  precofvallem  49355  prcof22a  49381