Theorem oveq1i 5851

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveq1i	⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Proof of Theorem oveq1i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq1 5848	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Syntax hints:   = wceq 1343  (class class class)co 5841

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844

This theorem is referenced by:  caov12  6026  map1  6774  halfnqq  7347  prarloclem5  7437  m1m1sr  7698  caucvgsrlemfv  7728  caucvgsr  7739  pitonnlem1  7782  axi2m1  7812  axcnre  7818  axcaucvg  7837  mvrraddi  8111  mvlladdi  8112  negsubdi  8150  mul02  8281  mulneg1  8289  mulreim  8498  recextlem1  8544  recdivap  8610  2p2e4  8980  2times  8981  3p2e5  8994  3p3e6  8995  4p2e6  8996  4p3e7  8997  4p4e8  8998  5p2e7  8999  5p3e8  9000  5p4e9  9001  6p2e8  9002  6p3e9  9003  7p2e9  9004  1mhlfehlf  9071  8th4div3  9072  halfpm6th  9073  nneoor  9289  9p1e10  9320  dfdec10  9321  num0h  9329  numsuc  9331  dec10p  9360  numma  9361  nummac  9362  numma2c  9363  numadd  9364  numaddc  9365  nummul2c  9367  decaddci  9378  decsubi  9380  decmul1  9381  5p5e10  9388  6p4e10  9389  7p3e10  9392  8p2e10  9397  decbin0  9457  decbin2  9458  elfzp1b  10028  elfzm1b  10029  fz01or  10042  fz1ssfz0  10048  fz0to4untppr  10055  qbtwnrelemcalc  10187  fldiv4p1lem1div2  10236  1tonninf  10371  mulexpzap  10491  expaddzap  10495  sq4e2t8  10548  cu2  10549  i3  10552  iexpcyc  10555  binom2i  10559  binom3  10568  3dec  10623  faclbnd  10650  bcm1k  10669  bcp1nk  10671  bcpasc  10675  hashp1i  10719  hashxp  10735  imre  10789  crim  10796  remullem  10809  resqrexlemfp1  10947  resqrexlemover  10948  resqrexlemcalc1  10952  resqrexlemnm  10956  absexpzap  11018  absimle  11022  amgm2  11056  maxabslemlub  11145  fsumconst  11391  modfsummod  11395  binomlem  11420  binom11  11423  arisum  11435  arisum2  11436  georeclim  11450  geo2sum  11451  mertenslemi1  11472  mertenslem2  11473  mertensabs  11474  prodfrecap  11483  fprodm1s  11538  fprodp1s  11539  fprodrec  11566  fprodmodd  11578  efzval  11620  resinval  11652  recosval  11653  efi4p  11654  tan0  11668  efival  11669  cosadd  11674  cos2tsin  11688  ef01bndlem  11693  cos1bnd  11696  cos2bnd  11697  absefib  11707  efieq1re  11708  demoivreALT  11710  eirraplem  11713  3dvdsdec  11798  3dvds2dec  11799  odd2np1  11806  nn0o1gt2  11838  nn0o  11840  flodddiv4  11867  algrp1  11974  3lcm2e6woprm  12014  nn0gcdsq  12128  phiprmpw  12150  prmdiv  12163  prmdiveq  12164  pythagtriplem1  12193  pythagtriplem12  12203  pythagtriplem14  12205  pockthi  12284  infpnlem1  12285  cnmpt1res  12896  rerestcntop  13150  dvfvalap  13250  dvcnp2cntop  13263  dveflem  13287  reeff1oleme  13293  sin0pilem1  13302  sinhalfpilem  13312  cospi  13321  eulerid  13323  cos2pi  13325  ef2kpi  13327  sinhalfpip  13341  sinhalfpim  13342  coshalfpip  13343  coshalfpim  13344  sincosq3sgn  13349  sincosq4sgn  13350  cosq23lt0  13354  tangtx  13359  sincos4thpi  13361  sincos6thpi  13363  cosq34lt1  13371  rplogb1  13466  2logb9irr  13489  sqrt2cxp2logb9e3  13493  2logb9irrap  13495  binom4  13497  lgsdir2lem1  13529  lgsdir2lem2  13530  lgsdir2lem4  13532  lgsdir2lem5  13533  lgsne0  13539  1lgs  13544  ex-fl  13566  ex-exp  13568  ex-bc  13570  012of  13835  2o01f  13836  qdencn  13866  isomninnlem  13869  iswomninnlem  13888  ismkvnnlem  13891