Theorem oveq1i 6028

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

Syntax hints:   = wceq 1397  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  caov12  6211  map1  6987  exmidpw2en  7104  halfnqq  7630  prarloclem5  7720  m1m1sr  7981  caucvgsrlemfv  8011  caucvgsr  8022  pitonnlem1  8065  axi2m1  8095  axcnre  8101  axcaucvg  8120  mvrraddi  8396  mvlladdi  8397  negsubdi  8435  mul02  8566  mulneg1  8574  mulreim  8784  recextlem1  8831  recdivap  8898  2p2e4  9270  2times  9271  3p2e5  9285  3p3e6  9286  4p2e6  9287  4p3e7  9288  4p4e8  9289  5p2e7  9290  5p3e8  9291  5p4e9  9292  6p2e8  9293  6p3e9  9294  7p2e9  9295  1mhlfehlf  9362  8th4div3  9363  halfpm6th  9364  nneoor  9582  9p1e10  9613  dfdec10  9614  num0h  9622  numsuc  9624  dec10p  9653  numma  9654  nummac  9655  numma2c  9656  numadd  9657  numaddc  9658  nummul2c  9660  decaddci  9671  decsubi  9673  decmul1  9674  5p5e10  9681  6p4e10  9682  7p3e10  9685  8p2e10  9690  decbin0  9750  decbin2  9751  elfzp1b  10332  elfzm1b  10333  fz01or  10346  fz1ssfz0  10352  fz0to4untppr  10359  qbtwnrelemcalc  10516  fldiv4p1lem1div2  10566  1tonninf  10704  mulexpzap  10842  expaddzap  10846  sq4e2t8  10900  cu2  10901  i3  10904  iexpcyc  10907  binom2i  10911  binom3  10920  3dec  10977  faclbnd  11004  bcm1k  11023  bcp1nk  11025  bcpasc  11029  hashp1i  11075  hashxp  11091  ccatlid  11187  pfxccatin12lem2c  11315  imre  11416  crim  11423  remullem  11436  resqrexlemfp1  11574  resqrexlemover  11575  resqrexlemcalc1  11579  resqrexlemnm  11583  absexpzap  11645  absimle  11649  amgm2  11683  maxabslemlub  11772  fsumconst  12020  modfsummod  12024  binomlem  12049  binom11  12052  arisum  12064  arisum2  12065  georeclim  12079  geo2sum  12080  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  prodfrecap  12112  fprodm1s  12167  fprodp1s  12168  fprodrec  12195  fprodmodd  12207  efzval  12249  resinval  12281  recosval  12282  efi4p  12283  tan0  12297  efival  12298  cosadd  12303  cos2tsin  12317  ef01bndlem  12322  cos1bnd  12325  cos2bnd  12326  absefib  12337  efieq1re  12338  demoivreALT  12340  eirraplem  12343  3dvds  12430  3dvdsdec  12431  3dvds2dec  12432  odd2np1  12439  nn0o1gt2  12471  nn0o  12473  5ndvds3  12500  5ndvds6  12501  flodddiv4  12502  m1bits  12526  algrp1  12623  3lcm2e6woprm  12663  nn0gcdsq  12777  phiprmpw  12799  prmdiv  12812  prmdiveq  12813  pythagtriplem1  12843  pythagtriplem12  12853  pythagtriplem14  12855  pockthi  12936  infpnlem1  12937  4sqlem12  12980  4sqlem13m  12981  4sqlem19  12987  dec5dvds  12990  dec5nprm  12992  dec2nprm  12993  modxai  12994  modxp1i  12996  modsubi  12997  gcdmodi  12999  decsplit0b  13004  decsplit1  13006  decsplit  13007  karatsuba  13008  2exp7  13012  2exp8  13013  3exp3  13016  pwsbas  13380  subsubm  13571  mulg2  13723  subsubg  13789  unitsubm  14139  subsubrng  14234  subsubrg  14265  lsslss  14401  expghmap  14627  cnmpt1res  15026  rerestcntop  15288  rerest  15290  dvfvalap  15411  dvcnp2cntop  15429  dveflem  15456  plyun0  15466  dvply1  15495  reeff1oleme  15502  sin0pilem1  15511  sinhalfpilem  15521  cospi  15530  eulerid  15532  cos2pi  15534  ef2kpi  15536  sinhalfpip  15550  sinhalfpim  15551  coshalfpip  15552  coshalfpim  15553  sincosq3sgn  15558  sincosq4sgn  15559  cosq23lt0  15563  tangtx  15568  sincos4thpi  15570  sincos6thpi  15572  cosq34lt1  15580  rplogb1  15678  2logb9irr  15701  sqrt2cxp2logb9e3  15705  2logb9irrap  15707  binom4  15709  lgsdir2lem1  15763  lgsdir2lem2  15764  lgsdir2lem4  15766  lgsdir2lem5  15767  lgsne0  15773  1lgs  15778  gausslemma2dlem0e  15788  gausslemma2dlem0f  15789  gausslemma2dlem3  15798  gausslemma2d  15804  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem3  15807  lgseisenlem4  15808  lgseisen  15809  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2lem1  15816  lgsquad2lem2  15817  m1lgs  15820  2lgslem3a  15828  2lgslem3b  15829  2lgslem3c  15830  2lgslem3d  15831  2lgsoddprmlem3a  15842  2lgsoddprmlem3b  15843  2lgsoddprmlem3c  15844  2lgsoddprmlem3d  15845  ex-fl  16343  ex-exp  16345  ex-bc  16347  depindlem1  16351  012of  16618  2o01f  16619  qdencn  16657  isomninnlem  16660  iswomninnlem  16680  ismkvnnlem  16683