Theorem fco2d

Description: Natural deduction form of fco2 . (Contributed by Stanislas Polu, 9-Mar-2020)

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

Proof

Step	Hyp	Ref	Expression
1		fco2d.1	$$⊢\phi \to G:A⟶B$$
2		fco2d.2	$$⊢\phi \to \left({F\upharpoonright }_B\right):B⟶C$$
3		fco2	$$⊢\left(\left({F\upharpoonright }_B\right):B⟶C\wedge G:A⟶B\right)\to \left(F\circ G\right):A⟶C$$
4	2 1 3	syl2anc	$$⊢\phi \to \left(F\circ G\right):A⟶C$$