Metamath Proof Explorer

Theorem 2fveq3

Description: Equality theorem for nested function values. (Contributed by AV, 14-Aug-2022)

Ref Expression
Assertion 2fveq3 
|- ( A = B -> ( F ` ( G ` A ) ) = ( F ` ( G ` B ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = B -> ( G ` A ) = ( G ` B ) )
2 1 fveq2d 
 |-  ( A = B -> ( F ` ( G ` A ) ) = ( F ` ( G ` B ) ) )