Theorem fco2d

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

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

Proof

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