Metamath Proof Explorer


Theorem 2fveq3

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

Ref Expression
Assertion 2fveq3 A=BFGA=FGB

Proof

Step Hyp Ref Expression
1 fveq2 A=BGA=GB
2 1 fveq2d A=BFGA=FGB