Metamath Proof Explorer


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 ) )