Theorem oveq1i 5935

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  caov12  6116  map1  6880  exmidpw2en  6982  halfnqq  7494  prarloclem5  7584  m1m1sr  7845  caucvgsrlemfv  7875  caucvgsr  7886  pitonnlem1  7929  axi2m1  7959  axcnre  7965  axcaucvg  7984  mvrraddi  8260  mvlladdi  8261  negsubdi  8299  mul02  8430  mulneg1  8438  mulreim  8648  recextlem1  8695  recdivap  8762  2p2e4  9134  2times  9135  3p2e5  9149  3p3e6  9150  4p2e6  9151  4p3e7  9152  4p4e8  9153  5p2e7  9154  5p3e8  9155  5p4e9  9156  6p2e8  9157  6p3e9  9158  7p2e9  9159  1mhlfehlf  9226  8th4div3  9227  halfpm6th  9228  nneoor  9445  9p1e10  9476  dfdec10  9477  num0h  9485  numsuc  9487  dec10p  9516  numma  9517  nummac  9518  numma2c  9519  numadd  9520  numaddc  9521  nummul2c  9523  decaddci  9534  decsubi  9536  decmul1  9537  5p5e10  9544  6p4e10  9545  7p3e10  9548  8p2e10  9553  decbin0  9613  decbin2  9614  elfzp1b  10189  elfzm1b  10190  fz01or  10203  fz1ssfz0  10209  fz0to4untppr  10216  qbtwnrelemcalc  10362  fldiv4p1lem1div2  10412  1tonninf  10550  mulexpzap  10688  expaddzap  10692  sq4e2t8  10746  cu2  10747  i3  10750  iexpcyc  10753  binom2i  10757  binom3  10766  3dec  10823  faclbnd  10850  bcm1k  10869  bcp1nk  10871  bcpasc  10875  hashp1i  10919  hashxp  10935  imre  11033  crim  11040  remullem  11053  resqrexlemfp1  11191  resqrexlemover  11192  resqrexlemcalc1  11196  resqrexlemnm  11200  absexpzap  11262  absimle  11266  amgm2  11300  maxabslemlub  11389  fsumconst  11636  modfsummod  11640  binomlem  11665  binom11  11668  arisum  11680  arisum2  11681  georeclim  11695  geo2sum  11696  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  prodfrecap  11728  fprodm1s  11783  fprodp1s  11784  fprodrec  11811  fprodmodd  11823  efzval  11865  resinval  11897  recosval  11898  efi4p  11899  tan0  11913  efival  11914  cosadd  11919  cos2tsin  11933  ef01bndlem  11938  cos1bnd  11941  cos2bnd  11942  absefib  11953  efieq1re  11954  demoivreALT  11956  eirraplem  11959  3dvds  12046  3dvdsdec  12047  3dvds2dec  12048  odd2np1  12055  nn0o1gt2  12087  nn0o  12089  5ndvds3  12116  5ndvds6  12117  flodddiv4  12118  m1bits  12142  algrp1  12239  3lcm2e6woprm  12279  nn0gcdsq  12393  phiprmpw  12415  prmdiv  12428  prmdiveq  12429  pythagtriplem1  12459  pythagtriplem12  12469  pythagtriplem14  12471  pockthi  12552  infpnlem1  12553  4sqlem12  12596  4sqlem13m  12597  4sqlem19  12603  dec5dvds  12606  dec5nprm  12608  dec2nprm  12609  modxai  12610  modxp1i  12612  modsubi  12613  gcdmodi  12615  decsplit0b  12620  decsplit1  12622  decsplit  12623  karatsuba  12624  2exp7  12628  2exp8  12629  3exp3  12632  pwsbas  12994  subsubm  13185  mulg2  13337  subsubg  13403  unitsubm  13751  subsubrng  13846  subsubrg  13877  lsslss  14013  expghmap  14239  cnmpt1res  14616  rerestcntop  14878  rerest  14880  dvfvalap  15001  dvcnp2cntop  15019  dveflem  15046  plyun0  15056  dvply1  15085  reeff1oleme  15092  sin0pilem1  15101  sinhalfpilem  15111  cospi  15120  eulerid  15122  cos2pi  15124  ef2kpi  15126  sinhalfpip  15140  sinhalfpim  15141  coshalfpip  15142  coshalfpim  15143  sincosq3sgn  15148  sincosq4sgn  15149  cosq23lt0  15153  tangtx  15158  sincos4thpi  15160  sincos6thpi  15162  cosq34lt1  15170  rplogb1  15268  2logb9irr  15291  sqrt2cxp2logb9e3  15295  2logb9irrap  15297  binom4  15299  lgsdir2lem1  15353  lgsdir2lem2  15354  lgsdir2lem4  15356  lgsdir2lem5  15357  lgsne0  15363  1lgs  15368  gausslemma2dlem0e  15378  gausslemma2dlem0f  15379  gausslemma2dlem3  15388  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgseisen  15399  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem1  15406  lgsquad2lem2  15407  m1lgs  15410  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgsoddprmlem3a  15432  2lgsoddprmlem3b  15433  2lgsoddprmlem3c  15434  2lgsoddprmlem3d  15435  ex-fl  15455  ex-exp  15457  ex-bc  15459  012of  15724  2o01f  15725  qdencn  15758  isomninnlem  15761  iswomninnlem  15780  ismkvnnlem  15783