Theorem oveq2i 5864

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveq2i	⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Proof of Theorem oveq2i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq2 5861	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Syntax hints:   = wceq 1348  (class class class)co 5853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856

This theorem is referenced by:  caov32  6040  oa1suc  6446  nnm1  6504  nnm2  6505  mapsnconst  6672  mapsncnv  6673  mulidnq  7351  halfnqq  7372  addpinq1  7426  addnqpr1  7524  caucvgprlemm  7630  caucvgprprlemval  7650  caucvgprprlemnbj  7655  caucvgprprlemmu  7657  caucvgprprlemaddq  7670  caucvgprprlem1  7671  caucvgprprlem2  7672  m1p1sr  7722  m1m1sr  7723  0idsr  7729  1idsr  7730  00sr  7731  pn0sr  7733  ltm1sr  7739  caucvgsrlemoffres  7762  caucvgsr  7764  mulresr  7800  pitonnlem2  7809  axi2m1  7837  ax1rid  7839  axcnre  7843  add42i  8085  negid  8166  negsub  8167  subneg  8168  negsubdii  8204  apreap  8506  recexaplem2  8570  muleqadd  8586  crap0  8874  2p2e4  9005  3p2e5  9019  3p3e6  9020  4p2e6  9021  4p3e7  9022  4p4e8  9023  5p2e7  9024  5p3e8  9025  5p4e9  9026  6p2e8  9027  6p3e9  9028  7p2e9  9029  3t3e9  9035  8th4div3  9097  halfpm6th  9098  iap0  9101  addltmul  9114  div4p1lem1div2  9131  peano2z  9248  nn0n0n1ge2  9282  nneoor  9314  zeo  9317  numsuc  9356  numltc  9368  numsucc  9382  numma  9386  nummul1c  9391  decrmac  9400  decsubi  9405  decmul1  9406  decmul10add  9411  6p5lem  9412  5p5e10  9413  6p4e10  9414  7p3e10  9417  8p2e10  9422  4t3lem  9439  9t11e99  9472  decbin2  9483  fztp  10034  fzprval  10038  fztpval  10039  fzshftral  10064  fz0tp  10078  fz0to3un2pr  10079  fzo01  10172  fzo12sn  10173  fzo0to2pr  10174  fzo0to3tp  10175  fzo0to42pr  10176  intqfrac2  10275  intfracq  10276  sqval  10534  sq4e2t8  10573  cu2  10574  i3  10577  i4  10578  binom2i  10584  binom3  10593  3dec  10648  faclbnd  10675  faclbnd2  10676  bcn1  10692  bcn2  10698  4bc3eq4  10707  4bc2eq6  10708  reim0  10825  cji  10866  resqrexlemover  10974  resqrexlemcalc1  10978  resqrexlemcalc3  10980  absi  11023  fsump1i  11396  fsumconst  11417  modfsummodlemstep  11420  arisum2  11462  geoihalfsum  11485  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  fprodconst  11583  fprodrec  11592  ef0lem  11623  ege2le3  11634  eft0val  11656  ef4p  11657  efgt1p2  11658  efgt1p  11659  tanval2ap  11676  efival  11695  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  cos1bnd  11722  cos2bnd  11723  3dvdsdec  11824  3dvds2dec  11825  odd2np1lem  11831  odd2np1  11832  oddp1even  11835  mod2eq1n2dvds  11838  opoe  11854  6gcd4e2  11950  lcmneg  12028  3lcm2e6woprm  12040  6lcm4e12  12041  3prm  12082  3lcm2e6  12114  sqrt2irrlem  12115  pw2dvdslemn  12119  phiprm  12177  prmdiv  12189  pythagtriplem12  12229  pythagtriplem14  12231  pcfac  12302  prmpwdvds  12307  pockthi  12310  4sqlem5  12334  restin  12970  uptx  13068  cnrehmeocntop  13387  dvexp  13469  dvmptidcn  13472  dvmptccn  13473  dveflem  13481  sinhalfpilem  13506  efhalfpi  13514  cospi  13515  efipi  13516  sin2pi  13518  cos2pi  13519  ef2pi  13520  sin2pim  13528  cos2pim  13529  sinmpi  13530  cosmpi  13531  sinppi  13532  cosppi  13533  sincosq4sgn  13544  tangtx  13553  sincos4thpi  13555  sincos6thpi  13557  sincos3rdpi  13558  abssinper  13561  cosq34lt1  13565  1cxp  13615  ecxp  13616  rpcxpsqrt  13636  rpelogb  13661  2logb9irrALT  13686  binom4  13691  lgslem1  13695  lgsdir2lem1  13723  lgsdir2lem2  13724  lgsdir2lem3  13725  lgsdir2lem5  13727  lgs1  13739  2sqlem8  13753  ex-exp  13762  ex-bc  13764  ex-gcd  13766  cvgcmp2nlemabs  14064