Theorem fcod 6741

Description: Composition of two mappings. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypotheses

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

Assertion

Ref	Expression
fcod	⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Proof of Theorem fcod

Step	Hyp	Ref	Expression
1		fcod.1	. 2 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
2		fcod.2	. 2 ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)
3		fco 6740	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∘ ccom 5669  ⟶wf 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5124  df-opab 5186  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-fun 6543  df-fn 6544  df-f 6545

This theorem is referenced by:  suppcoss  8214  mapen  9163  mapfienlem3  9429  mapfien  9430  cofsmo  10291  canthp1lem2  10675  gsumval3lem2  19892  psrass1lem  21906  psdmplcl  22114  mhmcompl  22332  comet  24470  dvcobr  25919  wrdpmcl  32862  gsumpart  32999  elrgspnlem1  33185  1arithidomlem2  33499  1arithidom  33500  subfacp1lem5  35148  metakunt33  42197  mapcod  42242  mhmcopsr  42522  selvvvval  42558  itcovalendof  48548  fucoid  49019