Theorem oveq2i 5785

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

Syntax hints:   = wceq 1331  (class class class)co 5774

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777

This theorem is referenced by:  caov32  5958  oa1suc  6363  nnm1  6420  nnm2  6421  mapsnconst  6588  mapsncnv  6589  mulidnq  7197  halfnqq  7218  addpinq1  7272  addnqpr1  7370  caucvgprlemm  7476  caucvgprprlemval  7496  caucvgprprlemnbj  7501  caucvgprprlemmu  7503  caucvgprprlemaddq  7516  caucvgprprlem1  7517  caucvgprprlem2  7518  m1p1sr  7568  m1m1sr  7569  0idsr  7575  1idsr  7576  00sr  7577  pn0sr  7579  ltm1sr  7585  caucvgsrlemoffres  7608  caucvgsr  7610  mulresr  7646  pitonnlem2  7655  axi2m1  7683  ax1rid  7685  axcnre  7689  add42i  7928  negid  8009  negsub  8010  subneg  8011  negsubdii  8047  apreap  8349  recexaplem2  8413  muleqadd  8429  crap0  8716  2p2e4  8847  3p2e5  8861  3p3e6  8862  4p2e6  8863  4p3e7  8864  4p4e8  8865  5p2e7  8866  5p3e8  8867  5p4e9  8868  6p2e8  8869  6p3e9  8870  7p2e9  8871  3t3e9  8877  8th4div3  8939  halfpm6th  8940  iap0  8943  addltmul  8956  div4p1lem1div2  8973  peano2z  9090  nn0n0n1ge2  9121  nneoor  9153  zeo  9156  numsuc  9195  numltc  9207  numsucc  9221  numma  9225  nummul1c  9230  decrmac  9239  decsubi  9244  decmul1  9245  decmul10add  9250  6p5lem  9251  5p5e10  9252  6p4e10  9253  7p3e10  9256  8p2e10  9261  4t3lem  9278  9t11e99  9311  decbin2  9322  fztp  9858  fzprval  9862  fztpval  9863  fzshftral  9888  fz0tp  9901  fzo01  9993  fzo12sn  9994  fzo0to2pr  9995  fzo0to3tp  9996  fzo0to42pr  9997  intqfrac2  10092  intfracq  10093  sqval  10351  sq4e2t8  10390  cu2  10391  i3  10394  i4  10395  binom2i  10401  binom3  10409  3dec  10461  faclbnd  10487  faclbnd2  10488  bcn1  10504  bcn2  10510  4bc3eq4  10519  4bc2eq6  10520  reim0  10633  cji  10674  resqrexlemover  10782  resqrexlemcalc1  10786  resqrexlemcalc3  10788  absi  10831  fsump1i  11202  fsumconst  11223  modfsummodlemstep  11226  arisum2  11268  geoihalfsum  11291  mertenslemi1  11304  mertenslem2  11305  mertensabs  11306  ef0lem  11366  ege2le3  11377  eft0val  11399  ef4p  11400  efgt1p2  11401  efgt1p  11402  tanval2ap  11420  efival  11439  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  cos1bnd  11466  cos2bnd  11467  3dvdsdec  11562  3dvds2dec  11563  odd2np1lem  11569  odd2np1  11570  oddp1even  11573  mod2eq1n2dvds  11576  opoe  11592  6gcd4e2  11683  lcmneg  11755  3lcm2e6woprm  11767  6lcm4e12  11768  3prm  11809  3lcm2e6  11838  sqrt2irrlem  11839  pw2dvdslemn  11843  phiprm  11899  restin  12345  uptx  12443  cnrehmeocntop  12762  dvexp  12844  dvmptidcn  12847  dvmptccn  12848  dveflem  12855  sinhalfpilem  12872  efhalfpi  12880  cospi  12881  efipi  12882  sin2pi  12884  cos2pi  12885  ef2pi  12886  sin2pim  12894  cos2pim  12895  sinmpi  12896  cosmpi  12897  sinppi  12898  cosppi  12899  sincosq4sgn  12910  tangtx  12919  sincos4thpi  12921  sincos6thpi  12923  sincos3rdpi  12924  abssinper  12927  cosq34lt1  12931  ex-exp  12939  ex-bc  12941  ex-gcd  12943  cvgcmp2nlemabs  13227