Theorem fcod

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

	Ref	Expression
Hypotheses	fcod.1	|- ( ph -> F : B --> C )
	fcod.2	|- ( ph -> G : A --> B )
Assertion	fcod	|- ( ph -> ( F o. G ) : A --> C )

Proof

Step	Hyp	Ref	Expression
1		fcod.1	|- ( ph -> F : B --> C )
2		fcod.2	|- ( ph -> G : A --> B )
3		fco	|- ( ( F : B --> C /\ G : A --> B ) -> ( F o. G ) : A --> C )
4	1 2 3	syl2anc	|- ( ph -> ( F o. G ) : A --> C )