Theorem oveq2i 5936

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

Hypothesis

Ref	Expression
oveq1i.1	|- A = B

Assertion

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

Proof of Theorem oveq2i

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

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

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 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  caov32  6115  oa1suc  6534  nnm1  6592  nnm2  6593  mapsnconst  6762  mapsncnv  6763  exmidpw2en  6982  mulidnq  7473  halfnqq  7494  addpinq1  7548  addnqpr1  7646  caucvgprlemm  7752  caucvgprprlemval  7772  caucvgprprlemnbj  7777  caucvgprprlemmu  7779  caucvgprprlemaddq  7792  caucvgprprlem1  7793  caucvgprprlem2  7794  m1p1sr  7844  m1m1sr  7845  0idsr  7851  1idsr  7852  00sr  7853  pn0sr  7855  ltm1sr  7861  caucvgsrlemoffres  7884  caucvgsr  7886  mulresr  7922  pitonnlem2  7931  axi2m1  7959  ax1rid  7961  axcnre  7965  add42i  8209  negid  8290  negsub  8291  subneg  8292  negsubdii  8328  apreap  8631  recexaplem2  8696  muleqadd  8712  crap0  9002  2p2e4  9134  3p2e5  9149  3p3e6  9150  4p2e6  9151  4p3e7  9152  4p4e8  9153  5p2e7  9154  5p3e8  9155  5p4e9  9156  6p2e8  9157  6p3e9  9158  7p2e9  9159  3t3e9  9165  8th4div3  9227  halfpm6th  9228  iap0  9231  addltmul  9245  div4p1lem1div2  9262  peano2z  9379  nn0n0n1ge2  9413  nneoor  9445  zeo  9448  numsuc  9487  numltc  9499  numsucc  9513  numma  9517  nummul1c  9522  decrmac  9531  decsubi  9536  decmul1  9537  decmul10add  9542  6p5lem  9543  5p5e10  9544  6p4e10  9545  7p3e10  9548  8p2e10  9553  4t3lem  9570  9t11e99  9603  decbin2  9614  fztp  10170  fzprval  10174  fztpval  10175  fzshftral  10200  fz0tp  10214  fz0to3un2pr  10215  fzo01  10309  fzo12sn  10310  fzo0to2pr  10311  fzo0to3tp  10312  fzo0to42pr  10313  intqfrac2  10428  intfracq  10429  xnn0nnen  10546  sqval  10706  sq4e2t8  10746  cu2  10747  i3  10750  i4  10751  binom2i  10757  binom3  10766  3dec  10823  faclbnd  10850  faclbnd2  10851  bcn1  10867  bcn2  10873  4bc3eq4  10882  4bc2eq6  10883  reim0  11043  cji  11084  resqrexlemover  11192  resqrexlemcalc1  11196  resqrexlemcalc3  11198  absi  11241  fsump1i  11615  fsumconst  11636  modfsummodlemstep  11639  arisum2  11681  geoihalfsum  11704  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  fprodconst  11802  fprodrec  11811  ef0lem  11842  ege2le3  11853  eft0val  11875  ef4p  11876  efgt1p2  11877  efgt1p  11878  tanval2ap  11895  efival  11914  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  cos1bnd  11941  cos2bnd  11942  3dvdsdec  12047  3dvds2dec  12048  odd2np1lem  12054  odd2np1  12055  oddp1even  12058  mod2eq1n2dvds  12061  opoe  12077  bits0  12130  0bits  12141  6gcd4e2  12187  lcmneg  12267  3lcm2e6woprm  12279  6lcm4e12  12280  3prm  12321  3lcm2e6  12353  sqrt2irrlem  12354  pw2dvdslemn  12358  phiprm  12416  prmdiv  12428  pythagtriplem12  12469  pythagtriplem14  12471  pcfac  12544  prmpwdvds  12549  pockthi  12552  4sqlem5  12576  4sqlem13m  12597  modxai  12610  gcdi  12614  numexpp1  12618  numexp2x  12619  decsplit0b  12620  decsplit1  12622  decsplit  12623  2exp5  12626  2exp7  12628  2exp11  12630  2exp16  12631  ressval2  12769  ecqusaddd  13444  gsumfzconstf  13548  znbas  14276  znzrh2  14278  restin  14496  uptx  14594  cnrehmeocntop  14930  hoverb  14968  dvexp  15031  dvmptidcn  15034  dvmptccn  15035  dvmptid  15036  dvmptc  15037  dvmptfsum  15045  dveflem  15046  plymullem1  15068  sinhalfpilem  15111  efhalfpi  15119  cospi  15120  efipi  15121  sin2pi  15123  cos2pi  15124  ef2pi  15125  sin2pim  15133  cos2pim  15134  sinmpi  15135  cosmpi  15136  sinppi  15137  cosppi  15138  sincosq4sgn  15149  tangtx  15158  sincos4thpi  15160  sincos6thpi  15162  sincos3rdpi  15163  abssinper  15166  cosq34lt1  15170  1cxp  15220  ecxp  15221  rpcxpsqrt  15242  rpelogb  15269  2logb9irrALT  15294  binom4  15299  1sgmprm  15314  lgslem1  15325  lgsdir2lem1  15353  lgsdir2lem2  15354  lgsdir2lem3  15355  lgsdir2lem5  15357  lgs1  15369  gausslemma2dlem1a  15383  gausslemma2dlem3  15388  gausslemma2dlem4  15389  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem3  15397  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2lem2  15407  m1lgs  15410  2lgslem1a2  15412  2sqlem8  15448  ex-exp  15457  ex-bc  15459  ex-gcd  15461  cvgcmp2nlemabs  15763