Theorem oveq2i 5847

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

Syntax hints:   = wceq 1342  (class class class)co 5836

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 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-rex 2448  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-iota 5147  df-fv 5190  df-ov 5839

This theorem is referenced by:  caov32  6020  oa1suc  6426  nnm1  6483  nnm2  6484  mapsnconst  6651  mapsncnv  6652  mulidnq  7321  halfnqq  7342  addpinq1  7396  addnqpr1  7494  caucvgprlemm  7600  caucvgprprlemval  7620  caucvgprprlemnbj  7625  caucvgprprlemmu  7627  caucvgprprlemaddq  7640  caucvgprprlem1  7641  caucvgprprlem2  7642  m1p1sr  7692  m1m1sr  7693  0idsr  7699  1idsr  7700  00sr  7701  pn0sr  7703  ltm1sr  7709  caucvgsrlemoffres  7732  caucvgsr  7734  mulresr  7770  pitonnlem2  7779  axi2m1  7807  ax1rid  7809  axcnre  7813  add42i  8055  negid  8136  negsub  8137  subneg  8138  negsubdii  8174  apreap  8476  recexaplem2  8540  muleqadd  8556  crap0  8844  2p2e4  8975  3p2e5  8989  3p3e6  8990  4p2e6  8991  4p3e7  8992  4p4e8  8993  5p2e7  8994  5p3e8  8995  5p4e9  8996  6p2e8  8997  6p3e9  8998  7p2e9  8999  3t3e9  9005  8th4div3  9067  halfpm6th  9068  iap0  9071  addltmul  9084  div4p1lem1div2  9101  peano2z  9218  nn0n0n1ge2  9252  nneoor  9284  zeo  9287  numsuc  9326  numltc  9338  numsucc  9352  numma  9356  nummul1c  9361  decrmac  9370  decsubi  9375  decmul1  9376  decmul10add  9381  6p5lem  9382  5p5e10  9383  6p4e10  9384  7p3e10  9387  8p2e10  9392  4t3lem  9409  9t11e99  9442  decbin2  9453  fztp  10003  fzprval  10007  fztpval  10008  fzshftral  10033  fz0tp  10047  fz0to3un2pr  10048  fzo01  10141  fzo12sn  10142  fzo0to2pr  10143  fzo0to3tp  10144  fzo0to42pr  10145  intqfrac2  10244  intfracq  10245  sqval  10503  sq4e2t8  10542  cu2  10543  i3  10546  i4  10547  binom2i  10553  binom3  10561  3dec  10616  faclbnd  10643  faclbnd2  10644  bcn1  10660  bcn2  10666  4bc3eq4  10675  4bc2eq6  10676  reim0  10789  cji  10830  resqrexlemover  10938  resqrexlemcalc1  10942  resqrexlemcalc3  10944  absi  10987  fsump1i  11360  fsumconst  11381  modfsummodlemstep  11384  arisum2  11426  geoihalfsum  11449  mertenslemi1  11462  mertenslem2  11463  mertensabs  11464  fprodconst  11547  fprodrec  11556  ef0lem  11587  ege2le3  11598  eft0val  11620  ef4p  11621  efgt1p2  11622  efgt1p  11623  tanval2ap  11640  efival  11659  ef01bndlem  11683  sin01bnd  11684  cos01bnd  11685  cos1bnd  11686  cos2bnd  11687  3dvdsdec  11787  3dvds2dec  11788  odd2np1lem  11794  odd2np1  11795  oddp1even  11798  mod2eq1n2dvds  11801  opoe  11817  6gcd4e2  11913  lcmneg  11985  3lcm2e6woprm  11997  6lcm4e12  11998  3prm  12039  3lcm2e6  12069  sqrt2irrlem  12070  pw2dvdslemn  12074  phiprm  12132  prmdiv  12144  pythagtriplem12  12184  pythagtriplem14  12186  pcfac  12257  restin  12717  uptx  12815  cnrehmeocntop  13134  dvexp  13216  dvmptidcn  13219  dvmptccn  13220  dveflem  13228  sinhalfpilem  13253  efhalfpi  13261  cospi  13262  efipi  13263  sin2pi  13265  cos2pi  13266  ef2pi  13267  sin2pim  13275  cos2pim  13276  sinmpi  13277  cosmpi  13278  sinppi  13279  cosppi  13280  sincosq4sgn  13291  tangtx  13300  sincos4thpi  13302  sincos6thpi  13304  sincos3rdpi  13305  abssinper  13308  cosq34lt1  13312  1cxp  13362  ecxp  13363  rpcxpsqrt  13383  rpelogb  13408  2logb9irrALT  13433  binom4  13438  ex-exp  13445  ex-bc  13447  ex-gcd  13449  cvgcmp2nlemabs  13745