Theorem oveq1i 5956

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 5953	. 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 1373  (class class class)co 5946

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949

This theorem is referenced by:  caov12  6137  map1  6906  exmidpw2en  7011  halfnqq  7525  prarloclem5  7615  m1m1sr  7876  caucvgsrlemfv  7906  caucvgsr  7917  pitonnlem1  7960  axi2m1  7990  axcnre  7996  axcaucvg  8015  mvrraddi  8291  mvlladdi  8292  negsubdi  8330  mul02  8461  mulneg1  8469  mulreim  8679  recextlem1  8726  recdivap  8793  2p2e4  9165  2times  9166  3p2e5  9180  3p3e6  9181  4p2e6  9182  4p3e7  9183  4p4e8  9184  5p2e7  9185  5p3e8  9186  5p4e9  9187  6p2e8  9188  6p3e9  9189  7p2e9  9190  1mhlfehlf  9257  8th4div3  9258  halfpm6th  9259  nneoor  9477  9p1e10  9508  dfdec10  9509  num0h  9517  numsuc  9519  dec10p  9548  numma  9549  nummac  9550  numma2c  9551  numadd  9552  numaddc  9553  nummul2c  9555  decaddci  9566  decsubi  9568  decmul1  9569  5p5e10  9576  6p4e10  9577  7p3e10  9580  8p2e10  9585  decbin0  9645  decbin2  9646  elfzp1b  10221  elfzm1b  10222  fz01or  10235  fz1ssfz0  10241  fz0to4untppr  10248  qbtwnrelemcalc  10400  fldiv4p1lem1div2  10450  1tonninf  10588  mulexpzap  10726  expaddzap  10730  sq4e2t8  10784  cu2  10785  i3  10788  iexpcyc  10791  binom2i  10795  binom3  10804  3dec  10861  faclbnd  10888  bcm1k  10907  bcp1nk  10909  bcpasc  10913  hashp1i  10957  hashxp  10973  ccatlid  11065  imre  11195  crim  11202  remullem  11215  resqrexlemfp1  11353  resqrexlemover  11354  resqrexlemcalc1  11358  resqrexlemnm  11362  absexpzap  11424  absimle  11428  amgm2  11462  maxabslemlub  11551  fsumconst  11798  modfsummod  11802  binomlem  11827  binom11  11830  arisum  11842  arisum2  11843  georeclim  11857  geo2sum  11858  mertenslemi1  11879  mertenslem2  11880  mertensabs  11881  prodfrecap  11890  fprodm1s  11945  fprodp1s  11946  fprodrec  11973  fprodmodd  11985  efzval  12027  resinval  12059  recosval  12060  efi4p  12061  tan0  12075  efival  12076  cosadd  12081  cos2tsin  12095  ef01bndlem  12100  cos1bnd  12103  cos2bnd  12104  absefib  12115  efieq1re  12116  demoivreALT  12118  eirraplem  12121  3dvds  12208  3dvdsdec  12209  3dvds2dec  12210  odd2np1  12217  nn0o1gt2  12249  nn0o  12251  5ndvds3  12278  5ndvds6  12279  flodddiv4  12280  m1bits  12304  algrp1  12401  3lcm2e6woprm  12441  nn0gcdsq  12555  phiprmpw  12577  prmdiv  12590  prmdiveq  12591  pythagtriplem1  12621  pythagtriplem12  12631  pythagtriplem14  12633  pockthi  12714  infpnlem1  12715  4sqlem12  12758  4sqlem13m  12759  4sqlem19  12765  dec5dvds  12768  dec5nprm  12770  dec2nprm  12771  modxai  12772  modxp1i  12774  modsubi  12775  gcdmodi  12777  decsplit0b  12782  decsplit1  12784  decsplit  12785  karatsuba  12786  2exp7  12790  2exp8  12791  3exp3  12794  pwsbas  13157  subsubm  13348  mulg2  13500  subsubg  13566  unitsubm  13914  subsubrng  14009  subsubrg  14040  lsslss  14176  expghmap  14402  cnmpt1res  14801  rerestcntop  15063  rerest  15065  dvfvalap  15186  dvcnp2cntop  15204  dveflem  15231  plyun0  15241  dvply1  15270  reeff1oleme  15277  sin0pilem1  15286  sinhalfpilem  15296  cospi  15305  eulerid  15307  cos2pi  15309  ef2kpi  15311  sinhalfpip  15325  sinhalfpim  15326  coshalfpip  15327  coshalfpim  15328  sincosq3sgn  15333  sincosq4sgn  15334  cosq23lt0  15338  tangtx  15343  sincos4thpi  15345  sincos6thpi  15347  cosq34lt1  15355  rplogb1  15453  2logb9irr  15476  sqrt2cxp2logb9e3  15480  2logb9irrap  15482  binom4  15484  lgsdir2lem1  15538  lgsdir2lem2  15539  lgsdir2lem4  15541  lgsdir2lem5  15542  lgsne0  15548  1lgs  15553  gausslemma2dlem0e  15563  gausslemma2dlem0f  15564  gausslemma2dlem3  15573  gausslemma2d  15579  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisenlem4  15583  lgseisen  15584  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem1  15591  lgsquad2lem2  15592  m1lgs  15595  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2lgsoddprmlem3a  15617  2lgsoddprmlem3b  15618  2lgsoddprmlem3c  15619  2lgsoddprmlem3d  15620  ex-fl  15698  ex-exp  15700  ex-bc  15702  012of  15967  2o01f  15968  qdencn  16003  isomninnlem  16006  iswomninnlem  16025  ismkvnnlem  16028