Theorem oveq1i 6010

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

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

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-iota 5277  df-fv 5325  df-ov 6003

This theorem is referenced by:  caov12  6193  map1  6963  exmidpw2en  7070  halfnqq  7593  prarloclem5  7683  m1m1sr  7944  caucvgsrlemfv  7974  caucvgsr  7985  pitonnlem1  8028  axi2m1  8058  axcnre  8064  axcaucvg  8083  mvrraddi  8359  mvlladdi  8360  negsubdi  8398  mul02  8529  mulneg1  8537  mulreim  8747  recextlem1  8794  recdivap  8861  2p2e4  9233  2times  9234  3p2e5  9248  3p3e6  9249  4p2e6  9250  4p3e7  9251  4p4e8  9252  5p2e7  9253  5p3e8  9254  5p4e9  9255  6p2e8  9256  6p3e9  9257  7p2e9  9258  1mhlfehlf  9325  8th4div3  9326  halfpm6th  9327  nneoor  9545  9p1e10  9576  dfdec10  9577  num0h  9585  numsuc  9587  dec10p  9616  numma  9617  nummac  9618  numma2c  9619  numadd  9620  numaddc  9621  nummul2c  9623  decaddci  9634  decsubi  9636  decmul1  9637  5p5e10  9644  6p4e10  9645  7p3e10  9648  8p2e10  9653  decbin0  9713  decbin2  9714  elfzp1b  10289  elfzm1b  10290  fz01or  10303  fz1ssfz0  10309  fz0to4untppr  10316  qbtwnrelemcalc  10470  fldiv4p1lem1div2  10520  1tonninf  10658  mulexpzap  10796  expaddzap  10800  sq4e2t8  10854  cu2  10855  i3  10858  iexpcyc  10861  binom2i  10865  binom3  10874  3dec  10931  faclbnd  10958  bcm1k  10977  bcp1nk  10979  bcpasc  10983  hashp1i  11027  hashxp  11043  ccatlid  11136  pfxccatin12lem2c  11257  imre  11357  crim  11364  remullem  11377  resqrexlemfp1  11515  resqrexlemover  11516  resqrexlemcalc1  11520  resqrexlemnm  11524  absexpzap  11586  absimle  11590  amgm2  11624  maxabslemlub  11713  fsumconst  11960  modfsummod  11964  binomlem  11989  binom11  11992  arisum  12004  arisum2  12005  georeclim  12019  geo2sum  12020  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  prodfrecap  12052  fprodm1s  12107  fprodp1s  12108  fprodrec  12135  fprodmodd  12147  efzval  12189  resinval  12221  recosval  12222  efi4p  12223  tan0  12237  efival  12238  cosadd  12243  cos2tsin  12257  ef01bndlem  12262  cos1bnd  12265  cos2bnd  12266  absefib  12277  efieq1re  12278  demoivreALT  12280  eirraplem  12283  3dvds  12370  3dvdsdec  12371  3dvds2dec  12372  odd2np1  12379  nn0o1gt2  12411  nn0o  12413  5ndvds3  12440  5ndvds6  12441  flodddiv4  12442  m1bits  12466  algrp1  12563  3lcm2e6woprm  12603  nn0gcdsq  12717  phiprmpw  12739  prmdiv  12752  prmdiveq  12753  pythagtriplem1  12783  pythagtriplem12  12793  pythagtriplem14  12795  pockthi  12876  infpnlem1  12877  4sqlem12  12920  4sqlem13m  12921  4sqlem19  12927  dec5dvds  12930  dec5nprm  12932  dec2nprm  12933  modxai  12934  modxp1i  12936  modsubi  12937  gcdmodi  12939  decsplit0b  12944  decsplit1  12946  decsplit  12947  karatsuba  12948  2exp7  12952  2exp8  12953  3exp3  12956  pwsbas  13320  subsubm  13511  mulg2  13663  subsubg  13729  unitsubm  14077  subsubrng  14172  subsubrg  14203  lsslss  14339  expghmap  14565  cnmpt1res  14964  rerestcntop  15226  rerest  15228  dvfvalap  15349  dvcnp2cntop  15367  dveflem  15394  plyun0  15404  dvply1  15433  reeff1oleme  15440  sin0pilem1  15449  sinhalfpilem  15459  cospi  15468  eulerid  15470  cos2pi  15472  ef2kpi  15474  sinhalfpip  15488  sinhalfpim  15489  coshalfpip  15490  coshalfpim  15491  sincosq3sgn  15496  sincosq4sgn  15497  cosq23lt0  15501  tangtx  15506  sincos4thpi  15508  sincos6thpi  15510  cosq34lt1  15518  rplogb1  15616  2logb9irr  15639  sqrt2cxp2logb9e3  15643  2logb9irrap  15645  binom4  15647  lgsdir2lem1  15701  lgsdir2lem2  15702  lgsdir2lem4  15704  lgsdir2lem5  15705  lgsne0  15711  1lgs  15716  gausslemma2dlem0e  15726  gausslemma2dlem0f  15727  gausslemma2dlem3  15736  gausslemma2d  15742  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgseisen  15747  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem1  15754  lgsquad2lem2  15755  m1lgs  15758  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgsoddprmlem3a  15780  2lgsoddprmlem3b  15781  2lgsoddprmlem3c  15782  2lgsoddprmlem3d  15783  ex-fl  16047  ex-exp  16049  ex-bc  16051  012of  16316  2o01f  16317  qdencn  16354  isomninnlem  16357  iswomninnlem  16376  ismkvnnlem  16379