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