Theorem oveq1i 5553

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 5550	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
3	1, 2	ax-mp 7	1 |- ( A F C ) = ( B F C )

Syntax hints:   = wceq 1285  (class class class)co 5543

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-iota 4897  df-fv 4940  df-ov 5546

This theorem is referenced by:  caov12  5720  halfnqq  6662  prarloclem5  6752  m1m1sr  7000  caucvgsrlemfv  7029  caucvgsr  7040  pitonnlem1  7075  axi2m1  7103  axcnre  7109  axcaucvg  7128  mvrraddi  7392  mvlladdi  7393  negsubdi  7431  mul02  7558  mulneg1  7566  mulreim  7771  recextlem1  7808  recdivap  7873  2p2e4  8226  2times  8227  3p2e5  8240  3p3e6  8241  4p2e6  8242  4p3e7  8243  4p4e8  8244  5p2e7  8245  5p3e8  8246  5p4e9  8247  6p2e8  8248  6p3e9  8249  7p2e9  8250  1mhlfehlf  8316  8th4div3  8317  halfpm6th  8318  nneoor  8530  9p1e10  8560  dfdec10  8561  num0h  8569  numsuc  8571  dec10p  8600  numma  8601  nummac  8602  numma2c  8603  numadd  8604  numaddc  8605  nummul2c  8607  decaddci  8618  decsubi  8620  decmul1  8621  5p5e10  8628  6p4e10  8629  7p3e10  8632  8p2e10  8637  decbin0  8697  decbin2  8698  elfzp1b  9190  elfzm1b  9191  fz01or  9204  qbtwnrelemcalc  9342  fldiv4p1lem1div2  9387  mulexpzap  9613  expaddzap  9617  cu2  9670  i3  9673  iexpcyc  9676  binom2i  9680  binom3  9687  3dec  9739  faclbnd  9765  bcm1k  9784  bcp1nk  9786  bcpasc  9790  sizep1i  9834  imre  9876  crim  9883  remullem  9896  resqrexlemfp1  10033  resqrexlemover  10034  resqrexlemcalc1  10038  resqrexlemnm  10042  absexpzap  10104  absimle  10108  amgm2  10142  maxabslemlub  10231  3dvdsdec  10409  3dvds2dec  10410  odd2np1  10417  nn0o1gt2  10449  nn0o  10451  flodddiv4  10478  3lcm2e6woprm  10612  nn0gcdsq  10722  ex-fl  10741  ex-bc  10744  qdencn  10970