Metamath Proof Explorer


Theorem feq123d

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

Ref Expression
Hypotheses feq12d.1 ( 𝜑𝐹 = 𝐺 )
feq12d.2 ( 𝜑𝐴 = 𝐵 )
feq123d.3 ( 𝜑𝐶 = 𝐷 )
Assertion feq123d ( 𝜑 → ( 𝐹 : 𝐴𝐶𝐺 : 𝐵𝐷 ) )

Proof

Step Hyp Ref Expression
1 feq12d.1 ( 𝜑𝐹 = 𝐺 )
2 feq12d.2 ( 𝜑𝐴 = 𝐵 )
3 feq123d.3 ( 𝜑𝐶 = 𝐷 )
4 1 2 feq12d ( 𝜑 → ( 𝐹 : 𝐴𝐶𝐺 : 𝐵𝐶 ) )
5 3 feq3d ( 𝜑 → ( 𝐺 : 𝐵𝐶𝐺 : 𝐵𝐷 ) )
6 4 5 bitrd ( 𝜑 → ( 𝐹 : 𝐴𝐶𝐺 : 𝐵𝐷 ) )