Theorem oveq2i 5906

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

Syntax hints:   = wceq 1364  (class class class)co 5895

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5898

This theorem is referenced by:  caov32  6083  oa1suc  6491  nnm1  6549  nnm2  6550  mapsnconst  6719  mapsncnv  6720  exmidpw2en  6939  mulidnq  7417  halfnqq  7438  addpinq1  7492  addnqpr1  7590  caucvgprlemm  7696  caucvgprprlemval  7716  caucvgprprlemnbj  7721  caucvgprprlemmu  7723  caucvgprprlemaddq  7736  caucvgprprlem1  7737  caucvgprprlem2  7738  m1p1sr  7788  m1m1sr  7789  0idsr  7795  1idsr  7796  00sr  7797  pn0sr  7799  ltm1sr  7805  caucvgsrlemoffres  7828  caucvgsr  7830  mulresr  7866  pitonnlem2  7875  axi2m1  7903  ax1rid  7905  axcnre  7909  add42i  8152  negid  8233  negsub  8234  subneg  8235  negsubdii  8271  apreap  8573  recexaplem2  8638  muleqadd  8654  crap0  8944  2p2e4  9075  3p2e5  9089  3p3e6  9090  4p2e6  9091  4p3e7  9092  4p4e8  9093  5p2e7  9094  5p3e8  9095  5p4e9  9096  6p2e8  9097  6p3e9  9098  7p2e9  9099  3t3e9  9105  8th4div3  9167  halfpm6th  9168  iap0  9171  addltmul  9184  div4p1lem1div2  9201  peano2z  9318  nn0n0n1ge2  9352  nneoor  9384  zeo  9387  numsuc  9426  numltc  9438  numsucc  9452  numma  9456  nummul1c  9461  decrmac  9470  decsubi  9475  decmul1  9476  decmul10add  9481  6p5lem  9482  5p5e10  9483  6p4e10  9484  7p3e10  9487  8p2e10  9492  4t3lem  9509  9t11e99  9542  decbin2  9553  fztp  10107  fzprval  10111  fztpval  10112  fzshftral  10137  fz0tp  10151  fz0to3un2pr  10152  fzo01  10245  fzo12sn  10246  fzo0to2pr  10247  fzo0to3tp  10248  fzo0to42pr  10249  intqfrac2  10349  intfracq  10350  sqval  10608  sq4e2t8  10648  cu2  10649  i3  10652  i4  10653  binom2i  10659  binom3  10668  3dec  10725  faclbnd  10752  faclbnd2  10753  bcn1  10769  bcn2  10775  4bc3eq4  10784  4bc2eq6  10785  reim0  10901  cji  10942  resqrexlemover  11050  resqrexlemcalc1  11054  resqrexlemcalc3  11056  absi  11099  fsump1i  11472  fsumconst  11493  modfsummodlemstep  11496  arisum2  11538  geoihalfsum  11561  mertenslemi1  11574  mertenslem2  11575  mertensabs  11576  fprodconst  11659  fprodrec  11668  ef0lem  11699  ege2le3  11710  eft0val  11732  ef4p  11733  efgt1p2  11734  efgt1p  11735  tanval2ap  11752  efival  11771  ef01bndlem  11795  sin01bnd  11796  cos01bnd  11797  cos1bnd  11798  cos2bnd  11799  3dvdsdec  11901  3dvds2dec  11902  odd2np1lem  11908  odd2np1  11909  oddp1even  11912  mod2eq1n2dvds  11915  opoe  11931  6gcd4e2  12027  lcmneg  12105  3lcm2e6woprm  12117  6lcm4e12  12118  3prm  12159  3lcm2e6  12191  sqrt2irrlem  12192  pw2dvdslemn  12196  phiprm  12254  prmdiv  12266  pythagtriplem12  12306  pythagtriplem14  12308  pcfac  12381  prmpwdvds  12386  pockthi  12389  4sqlem5  12413  4sqlem13m  12434  ressval2  12575  ecqusaddd  13174  znbas  13936  restin  14128  uptx  14226  cnrehmeocntop  14545  dvexp  14627  dvmptidcn  14630  dvmptccn  14631  dveflem  14639  sinhalfpilem  14664  efhalfpi  14672  cospi  14673  efipi  14674  sin2pi  14676  cos2pi  14677  ef2pi  14678  sin2pim  14686  cos2pim  14687  sinmpi  14688  cosmpi  14689  sinppi  14690  cosppi  14691  sincosq4sgn  14702  tangtx  14711  sincos4thpi  14713  sincos6thpi  14715  sincos3rdpi  14716  abssinper  14719  cosq34lt1  14723  1cxp  14773  ecxp  14774  rpcxpsqrt  14794  rpelogb  14819  2logb9irrALT  14844  binom4  14849  lgslem1  14854  lgsdir2lem1  14882  lgsdir2lem2  14883  lgsdir2lem3  14884  lgsdir2lem5  14886  lgs1  14898  lgseisenlem1  14903  m1lgs  14905  2sqlem8  14923  ex-exp  14932  ex-bc  14934  ex-gcd  14936  cvgcmp2nlemabs  15234