Theorem oveq1i 5932

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	|- A = B

Assertion

Ref	Expression
oveq1i	|- ( A F C ) = ( B F C )

Proof of Theorem oveq1i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 |- A = B
2		oveq1 5929	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
3	1, 2	ax-mp 5	1 |- ( A F C ) = ( B F C )

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

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 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925

This theorem is referenced by:  caov12  6112  map1  6871  exmidpw2en  6973  halfnqq  7477  prarloclem5  7567  m1m1sr  7828  caucvgsrlemfv  7858  caucvgsr  7869  pitonnlem1  7912  axi2m1  7942  axcnre  7948  axcaucvg  7967  mvrraddi  8243  mvlladdi  8244  negsubdi  8282  mul02  8413  mulneg1  8421  mulreim  8631  recextlem1  8678  recdivap  8745  2p2e4  9117  2times  9118  3p2e5  9132  3p3e6  9133  4p2e6  9134  4p3e7  9135  4p4e8  9136  5p2e7  9137  5p3e8  9138  5p4e9  9139  6p2e8  9140  6p3e9  9141  7p2e9  9142  1mhlfehlf  9209  8th4div3  9210  halfpm6th  9211  nneoor  9428  9p1e10  9459  dfdec10  9460  num0h  9468  numsuc  9470  dec10p  9499  numma  9500  nummac  9501  numma2c  9502  numadd  9503  numaddc  9504  nummul2c  9506  decaddci  9517  decsubi  9519  decmul1  9520  5p5e10  9527  6p4e10  9528  7p3e10  9531  8p2e10  9536  decbin0  9596  decbin2  9597  elfzp1b  10172  elfzm1b  10173  fz01or  10186  fz1ssfz0  10192  fz0to4untppr  10199  qbtwnrelemcalc  10345  fldiv4p1lem1div2  10395  1tonninf  10533  mulexpzap  10671  expaddzap  10675  sq4e2t8  10729  cu2  10730  i3  10733  iexpcyc  10736  binom2i  10740  binom3  10749  3dec  10806  faclbnd  10833  bcm1k  10852  bcp1nk  10854  bcpasc  10858  hashp1i  10902  hashxp  10918  imre  11016  crim  11023  remullem  11036  resqrexlemfp1  11174  resqrexlemover  11175  resqrexlemcalc1  11179  resqrexlemnm  11183  absexpzap  11245  absimle  11249  amgm2  11283  maxabslemlub  11372  fsumconst  11619  modfsummod  11623  binomlem  11648  binom11  11651  arisum  11663  arisum2  11664  georeclim  11678  geo2sum  11679  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  prodfrecap  11711  fprodm1s  11766  fprodp1s  11767  fprodrec  11794  fprodmodd  11806  efzval  11848  resinval  11880  recosval  11881  efi4p  11882  tan0  11896  efival  11897  cosadd  11902  cos2tsin  11916  ef01bndlem  11921  cos1bnd  11924  cos2bnd  11925  absefib  11936  efieq1re  11937  demoivreALT  11939  eirraplem  11942  3dvds  12029  3dvdsdec  12030  3dvds2dec  12031  odd2np1  12038  nn0o1gt2  12070  nn0o  12072  5ndvds3  12099  5ndvds6  12100  flodddiv4  12101  algrp1  12214  3lcm2e6woprm  12254  nn0gcdsq  12368  phiprmpw  12390  prmdiv  12403  prmdiveq  12404  pythagtriplem1  12434  pythagtriplem12  12444  pythagtriplem14  12446  pockthi  12527  infpnlem1  12528  4sqlem12  12571  4sqlem13m  12572  4sqlem19  12578  dec5dvds  12581  dec5nprm  12583  dec2nprm  12584  modxai  12585  modxp1i  12587  modsubi  12588  gcdmodi  12590  decsplit0b  12595  decsplit1  12597  decsplit  12598  karatsuba  12599  2exp7  12603  2exp8  12604  3exp3  12607  subsubm  13115  mulg2  13261  subsubg  13327  unitsubm  13675  subsubrng  13770  subsubrg  13801  lsslss  13937  expghmap  14163  cnmpt1res  14532  rerestcntop  14794  rerest  14796  dvfvalap  14917  dvcnp2cntop  14935  dveflem  14962  plyun0  14972  dvply1  15001  reeff1oleme  15008  sin0pilem1  15017  sinhalfpilem  15027  cospi  15036  eulerid  15038  cos2pi  15040  ef2kpi  15042  sinhalfpip  15056  sinhalfpim  15057  coshalfpip  15058  coshalfpim  15059  sincosq3sgn  15064  sincosq4sgn  15065  cosq23lt0  15069  tangtx  15074  sincos4thpi  15076  sincos6thpi  15078  cosq34lt1  15086  rplogb1  15184  2logb9irr  15207  sqrt2cxp2logb9e3  15211  2logb9irrap  15213  binom4  15215  lgsdir2lem1  15269  lgsdir2lem2  15270  lgsdir2lem4  15272  lgsdir2lem5  15273  lgsne0  15279  1lgs  15284  gausslemma2dlem0e  15294  gausslemma2dlem0f  15295  gausslemma2dlem3  15304  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem1  15322  lgsquad2lem2  15323  m1lgs  15326  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2lgsoddprmlem3a  15348  2lgsoddprmlem3b  15349  2lgsoddprmlem3c  15350  2lgsoddprmlem3d  15351  ex-fl  15371  ex-exp  15373  ex-bc  15375  012of  15640  2o01f  15641  qdencn  15671  isomninnlem  15674  iswomninnlem  15693  ismkvnnlem  15696