Theorem oveq2i 5881

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

Syntax hints:   = wceq 1353  (class class class)co 5870

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-br 4002  df-iota 5175  df-fv 5221  df-ov 5873

This theorem is referenced by:  caov32  6057  oa1suc  6463  nnm1  6521  nnm2  6522  mapsnconst  6689  mapsncnv  6690  mulidnq  7383  halfnqq  7404  addpinq1  7458  addnqpr1  7556  caucvgprlemm  7662  caucvgprprlemval  7682  caucvgprprlemnbj  7687  caucvgprprlemmu  7689  caucvgprprlemaddq  7702  caucvgprprlem1  7703  caucvgprprlem2  7704  m1p1sr  7754  m1m1sr  7755  0idsr  7761  1idsr  7762  00sr  7763  pn0sr  7765  ltm1sr  7771  caucvgsrlemoffres  7794  caucvgsr  7796  mulresr  7832  pitonnlem2  7841  axi2m1  7869  ax1rid  7871  axcnre  7875  add42i  8117  negid  8198  negsub  8199  subneg  8200  negsubdii  8236  apreap  8538  recexaplem2  8603  muleqadd  8619  crap0  8909  2p2e4  9040  3p2e5  9054  3p3e6  9055  4p2e6  9056  4p3e7  9057  4p4e8  9058  5p2e7  9059  5p3e8  9060  5p4e9  9061  6p2e8  9062  6p3e9  9063  7p2e9  9064  3t3e9  9070  8th4div3  9132  halfpm6th  9133  iap0  9136  addltmul  9149  div4p1lem1div2  9166  peano2z  9283  nn0n0n1ge2  9317  nneoor  9349  zeo  9352  numsuc  9391  numltc  9403  numsucc  9417  numma  9421  nummul1c  9426  decrmac  9435  decsubi  9440  decmul1  9441  decmul10add  9446  6p5lem  9447  5p5e10  9448  6p4e10  9449  7p3e10  9452  8p2e10  9457  4t3lem  9474  9t11e99  9507  decbin2  9518  fztp  10071  fzprval  10075  fztpval  10076  fzshftral  10101  fz0tp  10115  fz0to3un2pr  10116  fzo01  10209  fzo12sn  10210  fzo0to2pr  10211  fzo0to3tp  10212  fzo0to42pr  10213  intqfrac2  10312  intfracq  10313  sqval  10571  sq4e2t8  10610  cu2  10611  i3  10614  i4  10615  binom2i  10621  binom3  10630  3dec  10685  faclbnd  10712  faclbnd2  10713  bcn1  10729  bcn2  10735  4bc3eq4  10744  4bc2eq6  10745  reim0  10861  cji  10902  resqrexlemover  11010  resqrexlemcalc1  11014  resqrexlemcalc3  11016  absi  11059  fsump1i  11432  fsumconst  11453  modfsummodlemstep  11456  arisum2  11498  geoihalfsum  11521  mertenslemi1  11534  mertenslem2  11535  mertensabs  11536  fprodconst  11619  fprodrec  11628  ef0lem  11659  ege2le3  11670  eft0val  11692  ef4p  11693  efgt1p2  11694  efgt1p  11695  tanval2ap  11712  efival  11731  ef01bndlem  11755  sin01bnd  11756  cos01bnd  11757  cos1bnd  11758  cos2bnd  11759  3dvdsdec  11860  3dvds2dec  11861  odd2np1lem  11867  odd2np1  11868  oddp1even  11871  mod2eq1n2dvds  11874  opoe  11890  6gcd4e2  11986  lcmneg  12064  3lcm2e6woprm  12076  6lcm4e12  12077  3prm  12118  3lcm2e6  12150  sqrt2irrlem  12151  pw2dvdslemn  12155  phiprm  12213  prmdiv  12225  pythagtriplem12  12265  pythagtriplem14  12267  pcfac  12338  prmpwdvds  12343  pockthi  12346  4sqlem5  12370  ressval2  12516  restin  13458  uptx  13556  cnrehmeocntop  13875  dvexp  13957  dvmptidcn  13960  dvmptccn  13961  dveflem  13969  sinhalfpilem  13994  efhalfpi  14002  cospi  14003  efipi  14004  sin2pi  14006  cos2pi  14007  ef2pi  14008  sin2pim  14016  cos2pim  14017  sinmpi  14018  cosmpi  14019  sinppi  14020  cosppi  14021  sincosq4sgn  14032  tangtx  14041  sincos4thpi  14043  sincos6thpi  14045  sincos3rdpi  14046  abssinper  14049  cosq34lt1  14053  1cxp  14103  ecxp  14104  rpcxpsqrt  14124  rpelogb  14149  2logb9irrALT  14174  binom4  14179  lgslem1  14183  lgsdir2lem1  14211  lgsdir2lem2  14212  lgsdir2lem3  14213  lgsdir2lem5  14215  lgs1  14227  2sqlem8  14241  ex-exp  14250  ex-bc  14252  ex-gcd  14254  cvgcmp2nlemabs  14551