Theorem feq123d

Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Hypotheses	feq12d.1	$$⊢\phi \to F=G$$
	feq12d.2	$$⊢\phi \to A=B$$
	feq123d.3	$$⊢\phi \to C=D$$
Assertion	feq123d	$$⊢\phi \to \left(F:A⟶C\leftrightarrow G:B⟶D\right)$$

Proof

Step	Hyp	Ref	Expression
1		feq12d.1	$$⊢\phi \to F=G$$
2		feq12d.2	$$⊢\phi \to A=B$$
3		feq123d.3	$$⊢\phi \to C=D$$
4	1 2	feq12d	$$⊢\phi \to \left(F:A⟶C\leftrightarrow G:B⟶C\right)$$
5	3	feq3d	$$⊢\phi \to \left(G:B⟶C\leftrightarrow G:B⟶D\right)$$
6	4 5	bitrd	$$⊢\phi \to \left(F:A⟶C\leftrightarrow G:B⟶D\right)$$