Theorem oveq2i 5737

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 5734	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	ax-mp 7	1 ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Syntax hints:   = wceq 1312  (class class class)co 5726

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-rex 2394  df-v 2657  df-un 3039  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-iota 5044  df-fv 5087  df-ov 5729

This theorem is referenced by:  caov32  5910  oa1suc  6315  nnm1  6372  nnm2  6373  mapsnconst  6540  mapsncnv  6541  mulidnq  7139  halfnqq  7160  addpinq1  7214  addnqpr1  7312  caucvgprlemm  7418  caucvgprprlemval  7438  caucvgprprlemnbj  7443  caucvgprprlemmu  7445  caucvgprprlemaddq  7458  caucvgprprlem1  7459  caucvgprprlem2  7460  m1p1sr  7497  m1m1sr  7498  0idsr  7504  1idsr  7505  00sr  7506  pn0sr  7508  caucvgsrlemoffres  7536  caucvgsr  7538  mulresr  7567  pitonnlem2  7576  axi2m1  7604  ax1rid  7606  axcnre  7610  add42i  7845  negid  7926  negsub  7927  subneg  7928  negsubdii  7964  apreap  8261  recexaplem2  8320  muleqadd  8336  crap0  8620  2p2e4  8745  3p2e5  8759  3p3e6  8760  4p2e6  8761  4p3e7  8762  4p4e8  8763  5p2e7  8764  5p3e8  8765  5p4e9  8766  6p2e8  8767  6p3e9  8768  7p2e9  8769  3t3e9  8775  8th4div3  8837  halfpm6th  8838  iap0  8841  addltmul  8854  div4p1lem1div2  8871  peano2z  8988  nn0n0n1ge2  9019  nneoor  9051  zeo  9054  numsuc  9093  numltc  9105  numsucc  9119  numma  9123  nummul1c  9128  decrmac  9137  decsubi  9142  decmul1  9143  decmul10add  9148  6p5lem  9149  5p5e10  9150  6p4e10  9151  7p3e10  9154  8p2e10  9159  4t3lem  9176  9t11e99  9209  decbin2  9220  fztp  9745  fzprval  9749  fztpval  9750  fzshftral  9775  fz0tp  9788  fzo01  9880  fzo12sn  9881  fzo0to2pr  9882  fzo0to3tp  9883  fzo0to42pr  9884  intqfrac2  9979  intfracq  9980  sqval  10238  sq4e2t8  10277  cu2  10278  i3  10281  i4  10282  binom2i  10288  binom3  10296  3dec  10348  faclbnd  10374  faclbnd2  10375  bcn1  10391  bcn2  10397  4bc3eq4  10406  4bc2eq6  10407  reim0  10520  cji  10561  resqrexlemover  10668  resqrexlemcalc1  10672  resqrexlemcalc3  10674  absi  10717  fsump1i  11088  fsumconst  11109  modfsummodlemstep  11112  arisum2  11154  geoihalfsum  11177  mertenslemi1  11190  mertenslem2  11191  mertensabs  11192  ef0lem  11211  ege2le3  11222  eft0val  11244  ef4p  11245  efgt1p2  11246  efgt1p  11247  tanval2ap  11265  efival  11284  ef01bndlem  11308  sin01bnd  11309  cos01bnd  11310  cos1bnd  11311  cos2bnd  11312  3dvdsdec  11404  3dvds2dec  11405  odd2np1lem  11411  odd2np1  11412  oddp1even  11415  mod2eq1n2dvds  11418  opoe  11434  6gcd4e2  11523  lcmneg  11595  3lcm2e6woprm  11607  6lcm4e12  11608  3prm  11649  3lcm2e6  11678  sqrt2irrlem  11679  pw2dvdslemn  11682  phiprm  11738  restin  12182  uptx  12279  ex-exp  12623  ex-bc  12625  ex-gcd  12627  cvgcmp2nlemabs  12908