Theorem oveq2i 5929

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

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

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 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921

This theorem is referenced by:  caov32  6106  oa1suc  6520  nnm1  6578  nnm2  6579  mapsnconst  6748  mapsncnv  6749  exmidpw2en  6968  mulidnq  7449  halfnqq  7470  addpinq1  7524  addnqpr1  7622  caucvgprlemm  7728  caucvgprprlemval  7748  caucvgprprlemnbj  7753  caucvgprprlemmu  7755  caucvgprprlemaddq  7768  caucvgprprlem1  7769  caucvgprprlem2  7770  m1p1sr  7820  m1m1sr  7821  0idsr  7827  1idsr  7828  00sr  7829  pn0sr  7831  ltm1sr  7837  caucvgsrlemoffres  7860  caucvgsr  7862  mulresr  7898  pitonnlem2  7907  axi2m1  7935  ax1rid  7937  axcnre  7941  add42i  8185  negid  8266  negsub  8267  subneg  8268  negsubdii  8304  apreap  8606  recexaplem2  8671  muleqadd  8687  crap0  8977  2p2e4  9109  3p2e5  9123  3p3e6  9124  4p2e6  9125  4p3e7  9126  4p4e8  9127  5p2e7  9128  5p3e8  9129  5p4e9  9130  6p2e8  9131  6p3e9  9132  7p2e9  9133  3t3e9  9139  8th4div3  9201  halfpm6th  9202  iap0  9205  addltmul  9219  div4p1lem1div2  9236  peano2z  9353  nn0n0n1ge2  9387  nneoor  9419  zeo  9422  numsuc  9461  numltc  9473  numsucc  9487  numma  9491  nummul1c  9496  decrmac  9505  decsubi  9510  decmul1  9511  decmul10add  9516  6p5lem  9517  5p5e10  9518  6p4e10  9519  7p3e10  9522  8p2e10  9527  4t3lem  9544  9t11e99  9577  decbin2  9588  fztp  10144  fzprval  10148  fztpval  10149  fzshftral  10174  fz0tp  10188  fz0to3un2pr  10189  fzo01  10283  fzo12sn  10284  fzo0to2pr  10285  fzo0to3tp  10286  fzo0to42pr  10287  intqfrac2  10390  intfracq  10391  xnn0nnen  10508  sqval  10668  sq4e2t8  10708  cu2  10709  i3  10712  i4  10713  binom2i  10719  binom3  10728  3dec  10785  faclbnd  10812  faclbnd2  10813  bcn1  10829  bcn2  10835  4bc3eq4  10844  4bc2eq6  10845  reim0  11005  cji  11046  resqrexlemover  11154  resqrexlemcalc1  11158  resqrexlemcalc3  11160  absi  11203  fsump1i  11576  fsumconst  11597  modfsummodlemstep  11600  arisum2  11642  geoihalfsum  11665  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  fprodconst  11763  fprodrec  11772  ef0lem  11803  ege2le3  11814  eft0val  11836  ef4p  11837  efgt1p2  11838  efgt1p  11839  tanval2ap  11856  efival  11875  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  cos1bnd  11902  cos2bnd  11903  3dvdsdec  12006  3dvds2dec  12007  odd2np1lem  12013  odd2np1  12014  oddp1even  12017  mod2eq1n2dvds  12020  opoe  12036  6gcd4e2  12132  lcmneg  12212  3lcm2e6woprm  12224  6lcm4e12  12225  3prm  12266  3lcm2e6  12298  sqrt2irrlem  12299  pw2dvdslemn  12303  phiprm  12361  prmdiv  12373  pythagtriplem12  12413  pythagtriplem14  12415  pcfac  12488  prmpwdvds  12493  pockthi  12496  4sqlem5  12520  4sqlem13m  12541  ressval2  12684  ecqusaddd  13308  gsumfzconstf  13412  znbas  14132  znzrh2  14134  restin  14344  uptx  14442  cnrehmeocntop  14764  hoverb  14802  dvexp  14860  dvmptidcn  14863  dvmptccn  14864  dveflem  14872  plymullem1  14894  sinhalfpilem  14926  efhalfpi  14934  cospi  14935  efipi  14936  sin2pi  14938  cos2pi  14939  ef2pi  14940  sin2pim  14948  cos2pim  14949  sinmpi  14950  cosmpi  14951  sinppi  14952  cosppi  14953  sincosq4sgn  14964  tangtx  14973  sincos4thpi  14975  sincos6thpi  14977  sincos3rdpi  14978  abssinper  14981  cosq34lt1  14985  1cxp  15035  ecxp  15036  rpcxpsqrt  15056  rpelogb  15081  2logb9irrALT  15106  binom4  15111  lgslem1  15116  lgsdir2lem1  15144  lgsdir2lem2  15145  lgsdir2lem3  15146  lgsdir2lem5  15148  lgs1  15160  gausslemma2dlem1a  15174  gausslemma2dlem3  15179  gausslemma2dlem4  15180  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem3  15188  lgsquadlem1  15191  m1lgs  15192  2sqlem8  15210  ex-exp  15219  ex-bc  15221  ex-gcd  15223  cvgcmp2nlemabs  15522