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