Theorem feq3dd

Description: Equality deduction for functions. (Contributed by Thierry Arnoux, 27-May-2025)

	Ref	Expression
Hypotheses	feq3dd.eq	$$⊢\phi \to B=C$$
	feq3dd.f	$$⊢\phi \to F:A⟶B$$
Assertion	feq3dd	$$⊢\phi \to F:A⟶C$$

Proof

Step	Hyp	Ref	Expression
1		feq3dd.eq	$$⊢\phi \to B=C$$
2		feq3dd.f	$$⊢\phi \to F:A⟶B$$
3	1	feq3d	$$⊢\phi \to \left(F:A⟶B\leftrightarrow F:A⟶C\right)$$
4	2 3	mpbid	$$⊢\phi \to F:A⟶C$$