Theorem oveq2i 5978

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 5975	. 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 1373  (class class class)co 5967

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970

This theorem is referenced by:  caov32  6157  oa1suc  6576  nnm1  6634  nnm2  6635  mapsnconst  6804  mapsncnv  6805  exmidpw2en  7035  mulidnq  7537  halfnqq  7558  addpinq1  7612  addnqpr1  7710  caucvgprlemm  7816  caucvgprprlemval  7836  caucvgprprlemnbj  7841  caucvgprprlemmu  7843  caucvgprprlemaddq  7856  caucvgprprlem1  7857  caucvgprprlem2  7858  m1p1sr  7908  m1m1sr  7909  0idsr  7915  1idsr  7916  00sr  7917  pn0sr  7919  ltm1sr  7925  caucvgsrlemoffres  7948  caucvgsr  7950  mulresr  7986  pitonnlem2  7995  axi2m1  8023  ax1rid  8025  axcnre  8029  add42i  8273  negid  8354  negsub  8355  subneg  8356  negsubdii  8392  apreap  8695  recexaplem2  8760  muleqadd  8776  crap0  9066  2p2e4  9198  3p2e5  9213  3p3e6  9214  4p2e6  9215  4p3e7  9216  4p4e8  9217  5p2e7  9218  5p3e8  9219  5p4e9  9220  6p2e8  9221  6p3e9  9222  7p2e9  9223  3t3e9  9229  8th4div3  9291  halfpm6th  9292  iap0  9295  addltmul  9309  div4p1lem1div2  9326  peano2z  9443  nn0n0n1ge2  9478  nneoor  9510  zeo  9513  numsuc  9552  numltc  9564  numsucc  9578  numma  9582  nummul1c  9587  decrmac  9596  decsubi  9601  decmul1  9602  decmul10add  9607  6p5lem  9608  5p5e10  9609  6p4e10  9610  7p3e10  9613  8p2e10  9618  4t3lem  9635  9t11e99  9668  decbin2  9679  fztp  10235  fzprval  10239  fztpval  10240  fzshftral  10265  fz0tp  10279  fz0to3un2pr  10280  fzo01  10382  fzo12sn  10383  fzo0to2pr  10384  fzo0to3tp  10385  fzo0to42pr  10386  intqfrac2  10501  intfracq  10502  xnn0nnen  10619  sqval  10779  sq4e2t8  10819  cu2  10820  i3  10823  i4  10824  binom2i  10830  binom3  10839  3dec  10896  faclbnd  10923  faclbnd2  10924  bcn1  10940  bcn2  10946  4bc3eq4  10955  4bc2eq6  10956  ccatlid  11100  ccatrid  11101  pfx1  11194  pfxccatin12lem3  11223  pfxccatpfx1  11227  pfxccatpfx2  11228  reim0  11287  cji  11328  resqrexlemover  11436  resqrexlemcalc1  11440  resqrexlemcalc3  11442  absi  11485  fsump1i  11859  fsumconst  11880  modfsummodlemstep  11883  arisum2  11925  geoihalfsum  11948  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  fprodconst  12046  fprodrec  12055  ef0lem  12086  ege2le3  12097  eft0val  12119  ef4p  12120  efgt1p2  12121  efgt1p  12122  tanval2ap  12139  efival  12158  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  cos1bnd  12185  cos2bnd  12186  3dvdsdec  12291  3dvds2dec  12292  odd2np1lem  12298  odd2np1  12299  oddp1even  12302  mod2eq1n2dvds  12305  opoe  12321  bits0  12374  0bits  12385  6gcd4e2  12431  lcmneg  12511  3lcm2e6woprm  12523  6lcm4e12  12524  3prm  12565  3lcm2e6  12597  sqrt2irrlem  12598  pw2dvdslemn  12602  phiprm  12660  prmdiv  12672  pythagtriplem12  12713  pythagtriplem14  12715  pcfac  12788  prmpwdvds  12793  pockthi  12796  4sqlem5  12820  4sqlem13m  12841  modxai  12854  gcdi  12858  numexpp1  12862  numexp2x  12863  decsplit0b  12864  decsplit1  12866  decsplit  12867  2exp5  12870  2exp7  12872  2exp11  12874  2exp16  12875  ressval2  13013  ecqusaddd  13689  gsumfzconstf  13793  znbas  14521  znzrh2  14523  restin  14763  uptx  14861  cnrehmeocntop  15197  hoverb  15235  dvexp  15298  dvmptidcn  15301  dvmptccn  15302  dvmptid  15303  dvmptc  15304  dvmptfsum  15312  dveflem  15313  plymullem1  15335  sinhalfpilem  15378  efhalfpi  15386  cospi  15387  efipi  15388  sin2pi  15390  cos2pi  15391  ef2pi  15392  sin2pim  15400  cos2pim  15401  sinmpi  15402  cosmpi  15403  sinppi  15404  cosppi  15405  sincosq4sgn  15416  tangtx  15425  sincos4thpi  15427  sincos6thpi  15429  sincos3rdpi  15430  abssinper  15433  cosq34lt1  15437  1cxp  15487  ecxp  15488  rpcxpsqrt  15509  rpelogb  15536  2logb9irrALT  15561  binom4  15566  1sgmprm  15581  lgslem1  15592  lgsdir2lem1  15620  lgsdir2lem2  15621  lgsdir2lem3  15622  lgsdir2lem5  15624  lgs1  15636  gausslemma2dlem1a  15650  gausslemma2dlem3  15655  gausslemma2dlem4  15656  gausslemma2d  15661  lgseisenlem1  15662  lgseisenlem3  15664  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem2  15674  m1lgs  15677  2lgslem1a2  15679  2sqlem8  15715  ex-exp  15863  ex-bc  15865  ex-gcd  15867  cvgcmp2nlemabs  16173