Theorem oveq1i 6023

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

Syntax hints:   = wceq 1395  (class class class)co 6013

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  caov12  6206  map1  6982  exmidpw2en  7097  halfnqq  7620  prarloclem5  7710  m1m1sr  7971  caucvgsrlemfv  8001  caucvgsr  8012  pitonnlem1  8055  axi2m1  8085  axcnre  8091  axcaucvg  8110  mvrraddi  8386  mvlladdi  8387  negsubdi  8425  mul02  8556  mulneg1  8564  mulreim  8774  recextlem1  8821  recdivap  8888  2p2e4  9260  2times  9261  3p2e5  9275  3p3e6  9276  4p2e6  9277  4p3e7  9278  4p4e8  9279  5p2e7  9280  5p3e8  9281  5p4e9  9282  6p2e8  9283  6p3e9  9284  7p2e9  9285  1mhlfehlf  9352  8th4div3  9353  halfpm6th  9354  nneoor  9572  9p1e10  9603  dfdec10  9604  num0h  9612  numsuc  9614  dec10p  9643  numma  9644  nummac  9645  numma2c  9646  numadd  9647  numaddc  9648  nummul2c  9650  decaddci  9661  decsubi  9663  decmul1  9664  5p5e10  9671  6p4e10  9672  7p3e10  9675  8p2e10  9680  decbin0  9740  decbin2  9741  elfzp1b  10322  elfzm1b  10323  fz01or  10336  fz1ssfz0  10342  fz0to4untppr  10349  qbtwnrelemcalc  10505  fldiv4p1lem1div2  10555  1tonninf  10693  mulexpzap  10831  expaddzap  10835  sq4e2t8  10889  cu2  10890  i3  10893  iexpcyc  10896  binom2i  10900  binom3  10909  3dec  10966  faclbnd  10993  bcm1k  11012  bcp1nk  11014  bcpasc  11018  hashp1i  11064  hashxp  11080  ccatlid  11173  pfxccatin12lem2c  11301  imre  11402  crim  11409  remullem  11422  resqrexlemfp1  11560  resqrexlemover  11561  resqrexlemcalc1  11565  resqrexlemnm  11569  absexpzap  11631  absimle  11635  amgm2  11669  maxabslemlub  11758  fsumconst  12005  modfsummod  12009  binomlem  12034  binom11  12037  arisum  12049  arisum2  12050  georeclim  12064  geo2sum  12065  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  prodfrecap  12097  fprodm1s  12152  fprodp1s  12153  fprodrec  12180  fprodmodd  12192  efzval  12234  resinval  12266  recosval  12267  efi4p  12268  tan0  12282  efival  12283  cosadd  12288  cos2tsin  12302  ef01bndlem  12307  cos1bnd  12310  cos2bnd  12311  absefib  12322  efieq1re  12323  demoivreALT  12325  eirraplem  12328  3dvds  12415  3dvdsdec  12416  3dvds2dec  12417  odd2np1  12424  nn0o1gt2  12456  nn0o  12458  5ndvds3  12485  5ndvds6  12486  flodddiv4  12487  m1bits  12511  algrp1  12608  3lcm2e6woprm  12648  nn0gcdsq  12762  phiprmpw  12784  prmdiv  12797  prmdiveq  12798  pythagtriplem1  12828  pythagtriplem12  12838  pythagtriplem14  12840  pockthi  12921  infpnlem1  12922  4sqlem12  12965  4sqlem13m  12966  4sqlem19  12972  dec5dvds  12975  dec5nprm  12977  dec2nprm  12978  modxai  12979  modxp1i  12981  modsubi  12982  gcdmodi  12984  decsplit0b  12989  decsplit1  12991  decsplit  12992  karatsuba  12993  2exp7  12997  2exp8  12998  3exp3  13001  pwsbas  13365  subsubm  13556  mulg2  13708  subsubg  13774  unitsubm  14123  subsubrng  14218  subsubrg  14249  lsslss  14385  expghmap  14611  cnmpt1res  15010  rerestcntop  15272  rerest  15274  dvfvalap  15395  dvcnp2cntop  15413  dveflem  15440  plyun0  15450  dvply1  15479  reeff1oleme  15486  sin0pilem1  15495  sinhalfpilem  15505  cospi  15514  eulerid  15516  cos2pi  15518  ef2kpi  15520  sinhalfpip  15534  sinhalfpim  15535  coshalfpip  15536  coshalfpim  15537  sincosq3sgn  15542  sincosq4sgn  15543  cosq23lt0  15547  tangtx  15552  sincos4thpi  15554  sincos6thpi  15556  cosq34lt1  15564  rplogb1  15662  2logb9irr  15685  sqrt2cxp2logb9e3  15689  2logb9irrap  15691  binom4  15693  lgsdir2lem1  15747  lgsdir2lem2  15748  lgsdir2lem4  15750  lgsdir2lem5  15751  lgsne0  15757  1lgs  15762  gausslemma2dlem0e  15772  gausslemma2dlem0f  15773  gausslemma2dlem3  15782  gausslemma2d  15788  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem1  15800  lgsquad2lem2  15801  m1lgs  15804  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgsoddprmlem3a  15826  2lgsoddprmlem3b  15827  2lgsoddprmlem3c  15828  2lgsoddprmlem3d  15829  ex-fl  16257  ex-exp  16259  ex-bc  16261  012of  16528  2o01f  16529  qdencn  16567  isomninnlem  16570  iswomninnlem  16589  ismkvnnlem  16592