Theorem fcod

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

	Ref	Expression
Hypotheses	fcod.1	$$⊢\phi \to F:B⟶C$$
	fcod.2	$$⊢\phi \to G:A⟶B$$
Assertion	fcod	$$⊢\phi \to \left(F\circ G\right):A⟶C$$

Proof

Step	Hyp	Ref	Expression
1		fcod.1	$$⊢\phi \to F:B⟶C$$
2		fcod.2	$$⊢\phi \to G:A⟶B$$
3		fco	$$⊢\left(F:B⟶C\wedge G:A⟶B\right)\to \left(F\circ G\right):A⟶C$$
4	1 2 3	syl2anc	$$⊢\phi \to \left(F\circ G\right):A⟶C$$