Theorem fcod 6727

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 6726	. 2 ⊢ ((𝐹:𝐵⟶𝐶 ∧ 𝐺:𝐴⟶𝐵) → (𝐹 ∘ 𝐺):𝐴⟶𝐶)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐹 ∘ 𝐺):𝐴⟶𝐶)

This proof depends on syntax axioms:   → wi 4   ∘ ccom 5655  ⟶wf 6527

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6533  df-fn 6534  df-f 6535

This theorem is used by:  suppcoss  8208  mapen  9144  mapfienlem3  9383  mapfien  9384  cofsmo  10328  canthp1lem2  10719  gsumval3lem2  20100  psrass1lem  22221  mhmcompl  22410  selvvvval  22431  psdmplcl  22463  comet  24812  dvcobr  26246  wrdpmcl  33487  gsumpart  33606  elrgspnlem1  33785  1arithidomlem2  34050  1arithidom  34051  mplasclco  34130  mplvrpmlem  34157  mplvrpmfgalem  34158  mplvrpmga  34159  mplvrpmmhm  34160  mplvrpmrhm  34161  mplmonprod  34168  esplympl  34181  esplysply  34185  subfacp1lem5  35918  mapcod  43262  mhmcopsr  43570  chnsubseqword  47832  upgrimwlklem4  48942  itcovalendof  49725  fucoid  50400