This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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