Theorem 2fveq3 5605

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

Assertion

Ref	Expression
2fveq3	⊢ (𝐴 = 𝐵 → (𝐹‘(𝐺‘𝐴)) = (𝐹‘(𝐺‘𝐵)))

Proof of Theorem 2fveq3

Step	Hyp	Ref	Expression
1		fveq2 5600	. 2 ⊢ (𝐴 = 𝐵 → (𝐺‘𝐴) = (𝐺‘𝐵))
2	1	fveq2d 5604	1 ⊢ (𝐴 = 𝐵 → (𝐹‘(𝐺‘𝐴)) = (𝐹‘(𝐺‘𝐵)))

Syntax hints:   → wi 4   = wceq 1373  ‘cfv 5291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2779  df-un 3179  df-sn 3650  df-pr 3651  df-op 3653  df-uni 3866  df-br 4061  df-iota 5252  df-fv 5299

This theorem is referenced by:  difinfsnlem  7229  ctssdclemn0  7240  cc2  7416  seq3f1olemqsum  10697  seq3f1oleml  10700  seq3f1o  10701  seq3homo  10711  seqhomog  10714  seq3coll  11026  fsumf1o  11862  iserabs  11947  explecnv  11977  cvgratnnlemnexp  11996  cvgratnnlemmn  11997  fprodf1o  12060  nninfctlemfo  12522  alginv  12530  algcvg  12531  algcvga  12534  ctiunctlemu1st  12966  ctiunctlemu2nd  12967  ctiunctlemudc  12969  ctiunctlemfo  12971  prdsbasprj  13275  prdsplusgfval  13277  prdsmulrfval  13279  prdsbas3  13280  prdsinvlem  13601  isunitd  14029  subctctexmid  16247