Theorem fco2d

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

	Ref	Expression
Hypotheses	fco2d.1	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
	fco2d.2	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 )
Assertion	fco2d	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fco2d.1	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
2		fco2d.2	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 )
3		fco2	⊢ ( ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )
4	2 1 3	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 )