Theorem feq123d

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

	Ref	Expression
Hypotheses	feq12d.1	|- ( ph -> F = G )
	feq12d.2	|- ( ph -> A = B )
	feq123d.3	|- ( ph -> C = D )
Assertion	feq123d	|- ( ph -> ( F : A --> C <-> G : B --> D ) )

Proof

Step	Hyp	Ref	Expression
1		feq12d.1	|- ( ph -> F = G )
2		feq12d.2	|- ( ph -> A = B )
3		feq123d.3	|- ( ph -> C = D )
4	1 2	feq12d	|- ( ph -> ( F : A --> C <-> G : B --> C ) )
5	3	feq3d	|- ( ph -> ( G : B --> C <-> G : B --> D ) )
6	4 5	bitrd	|- ( ph -> ( F : A --> C <-> G : B --> D ) )