Theorem oveq1i 5887

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

Syntax hints:   = wceq 1353  (class class class)co 5877

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880

This theorem is referenced by:  caov12  6065  map1  6814  halfnqq  7411  prarloclem5  7501  m1m1sr  7762  caucvgsrlemfv  7792  caucvgsr  7803  pitonnlem1  7846  axi2m1  7876  axcnre  7882  axcaucvg  7901  mvrraddi  8176  mvlladdi  8177  negsubdi  8215  mul02  8346  mulneg1  8354  mulreim  8563  recextlem1  8610  recdivap  8677  2p2e4  9048  2times  9049  3p2e5  9062  3p3e6  9063  4p2e6  9064  4p3e7  9065  4p4e8  9066  5p2e7  9067  5p3e8  9068  5p4e9  9069  6p2e8  9070  6p3e9  9071  7p2e9  9072  1mhlfehlf  9139  8th4div3  9140  halfpm6th  9141  nneoor  9357  9p1e10  9388  dfdec10  9389  num0h  9397  numsuc  9399  dec10p  9428  numma  9429  nummac  9430  numma2c  9431  numadd  9432  numaddc  9433  nummul2c  9435  decaddci  9446  decsubi  9448  decmul1  9449  5p5e10  9456  6p4e10  9457  7p3e10  9460  8p2e10  9465  decbin0  9525  decbin2  9526  elfzp1b  10099  elfzm1b  10100  fz01or  10113  fz1ssfz0  10119  fz0to4untppr  10126  qbtwnrelemcalc  10258  fldiv4p1lem1div2  10307  1tonninf  10442  mulexpzap  10562  expaddzap  10566  sq4e2t8  10620  cu2  10621  i3  10624  iexpcyc  10627  binom2i  10631  binom3  10640  3dec  10696  faclbnd  10723  bcm1k  10742  bcp1nk  10744  bcpasc  10748  hashp1i  10792  hashxp  10808  imre  10862  crim  10869  remullem  10882  resqrexlemfp1  11020  resqrexlemover  11021  resqrexlemcalc1  11025  resqrexlemnm  11029  absexpzap  11091  absimle  11095  amgm2  11129  maxabslemlub  11218  fsumconst  11464  modfsummod  11468  binomlem  11493  binom11  11496  arisum  11508  arisum2  11509  georeclim  11523  geo2sum  11524  mertenslemi1  11545  mertenslem2  11546  mertensabs  11547  prodfrecap  11556  fprodm1s  11611  fprodp1s  11612  fprodrec  11639  fprodmodd  11651  efzval  11693  resinval  11725  recosval  11726  efi4p  11727  tan0  11741  efival  11742  cosadd  11747  cos2tsin  11761  ef01bndlem  11766  cos1bnd  11769  cos2bnd  11770  absefib  11780  efieq1re  11781  demoivreALT  11783  eirraplem  11786  3dvdsdec  11872  3dvds2dec  11873  odd2np1  11880  nn0o1gt2  11912  nn0o  11914  flodddiv4  11941  algrp1  12048  3lcm2e6woprm  12088  nn0gcdsq  12202  phiprmpw  12224  prmdiv  12237  prmdiveq  12238  pythagtriplem1  12267  pythagtriplem12  12277  pythagtriplem14  12279  pockthi  12358  infpnlem1  12359  mulg2  12997  subsubg  13062  unitsubm  13293  subsubrg  13371  lsslss  13473  cnmpt1res  13881  rerestcntop  14135  dvfvalap  14235  dvcnp2cntop  14248  dveflem  14272  reeff1oleme  14278  sin0pilem1  14287  sinhalfpilem  14297  cospi  14306  eulerid  14308  cos2pi  14310  ef2kpi  14312  sinhalfpip  14326  sinhalfpim  14327  coshalfpip  14328  coshalfpim  14329  sincosq3sgn  14334  sincosq4sgn  14335  cosq23lt0  14339  tangtx  14344  sincos4thpi  14346  sincos6thpi  14348  cosq34lt1  14356  rplogb1  14451  2logb9irr  14474  sqrt2cxp2logb9e3  14478  2logb9irrap  14480  binom4  14482  lgsdir2lem1  14514  lgsdir2lem2  14515  lgsdir2lem4  14517  lgsdir2lem5  14518  lgsne0  14524  1lgs  14529  lgseisenlem1  14535  lgseisenlem2  14536  m1lgs  14537  2lgsoddprmlem3a  14540  2lgsoddprmlem3b  14541  2lgsoddprmlem3c  14542  2lgsoddprmlem3d  14543  ex-fl  14562  ex-exp  14564  ex-bc  14566  012of  14830  2o01f  14831  qdencn  14860  isomninnlem  14863  iswomninnlem  14882  ismkvnnlem  14885