Theorem oveq2i 6029

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

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveq2i	⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Proof of Theorem oveq2i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq2 6026	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Syntax hints:   = wceq 1397  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  caov32  6210  oa1suc  6635  nnm1  6693  nnm2  6694  mapsnconst  6863  mapsncnv  6864  exmidpw2en  7104  mulidnq  7609  halfnqq  7630  addpinq1  7684  addnqpr1  7782  caucvgprlemm  7888  caucvgprprlemval  7908  caucvgprprlemnbj  7913  caucvgprprlemmu  7915  caucvgprprlemaddq  7928  caucvgprprlem1  7929  caucvgprprlem2  7930  m1p1sr  7980  m1m1sr  7981  0idsr  7987  1idsr  7988  00sr  7989  pn0sr  7991  ltm1sr  7997  caucvgsrlemoffres  8020  caucvgsr  8022  mulresr  8058  pitonnlem2  8067  axi2m1  8095  ax1rid  8097  axcnre  8101  add42i  8345  negid  8426  negsub  8427  subneg  8428  negsubdii  8464  apreap  8767  recexaplem2  8832  muleqadd  8848  crap0  9138  2p2e4  9270  3p2e5  9285  3p3e6  9286  4p2e6  9287  4p3e7  9288  4p4e8  9289  5p2e7  9290  5p3e8  9291  5p4e9  9292  6p2e8  9293  6p3e9  9294  7p2e9  9295  3t3e9  9301  8th4div3  9363  halfpm6th  9364  iap0  9367  addltmul  9381  div4p1lem1div2  9398  peano2z  9515  nn0n0n1ge2  9550  nneoor  9582  zeo  9585  numsuc  9624  numltc  9636  numsucc  9650  numma  9654  nummul1c  9659  decrmac  9668  decsubi  9673  decmul1  9674  decmul10add  9679  6p5lem  9680  5p5e10  9681  6p4e10  9682  7p3e10  9685  8p2e10  9690  4t3lem  9707  9t11e99  9740  decbin2  9751  fztp  10313  fzprval  10317  fztpval  10318  fzshftral  10343  fz0tp  10357  fz0to3un2pr  10358  fzo01  10461  fzo12sn  10462  fzo0to2pr  10463  fzo0to3tp  10464  fzo0to42pr  10465  intqfrac2  10581  intfracq  10582  xnn0nnen  10699  sqval  10859  sq4e2t8  10899  cu2  10900  i3  10903  i4  10904  binom2i  10910  binom3  10919  3dec  10976  faclbnd  11003  faclbnd2  11004  bcn1  11020  bcn2  11026  4bc3eq4  11035  4bc2eq6  11036  ccatlid  11183  ccatrid  11184  pfx1  11284  pfxccatin12lem3  11313  pfxccatpfx1  11317  pfxccatpfx2  11318  cats1fvn  11345  cats1catd  11349  cats2catd  11350  reim0  11422  cji  11463  resqrexlemover  11571  resqrexlemcalc1  11575  resqrexlemcalc3  11577  absi  11620  fsump1i  11995  fsumconst  12016  modfsummodlemstep  12019  arisum2  12061  geoihalfsum  12084  mertenslemi1  12097  mertenslem2  12098  mertensabs  12099  fprodconst  12182  fprodrec  12191  ef0lem  12222  ege2le3  12233  eft0val  12255  ef4p  12256  efgt1p2  12257  efgt1p  12258  tanval2ap  12275  efival  12294  ef01bndlem  12318  sin01bnd  12319  cos01bnd  12320  cos1bnd  12321  cos2bnd  12322  3dvdsdec  12427  3dvds2dec  12428  odd2np1lem  12434  odd2np1  12435  oddp1even  12438  mod2eq1n2dvds  12441  opoe  12457  bits0  12510  0bits  12521  6gcd4e2  12567  lcmneg  12647  3lcm2e6woprm  12659  6lcm4e12  12660  3prm  12701  3lcm2e6  12733  sqrt2irrlem  12734  pw2dvdslemn  12738  phiprm  12796  prmdiv  12808  pythagtriplem12  12849  pythagtriplem14  12851  pcfac  12924  prmpwdvds  12929  pockthi  12932  4sqlem5  12956  4sqlem13m  12977  modxai  12990  gcdi  12994  numexpp1  12998  numexp2x  12999  decsplit0b  13000  decsplit1  13002  decsplit  13003  2exp5  13006  2exp7  13008  2exp11  13010  2exp16  13011  ressval2  13150  ecqusaddd  13826  gsumfzconstf  13930  znbas  14660  znzrh2  14662  restin  14902  uptx  15000  cnrehmeocntop  15336  hoverb  15374  dvexp  15437  dvmptidcn  15440  dvmptccn  15441  dvmptid  15442  dvmptc  15443  dvmptfsum  15451  dveflem  15452  plymullem1  15474  sinhalfpilem  15517  efhalfpi  15525  cospi  15526  efipi  15527  sin2pi  15529  cos2pi  15530  ef2pi  15531  sin2pim  15539  cos2pim  15540  sinmpi  15541  cosmpi  15542  sinppi  15543  cosppi  15544  sincosq4sgn  15555  tangtx  15564  sincos4thpi  15566  sincos6thpi  15568  sincos3rdpi  15569  abssinper  15572  cosq34lt1  15576  1cxp  15626  ecxp  15627  rpcxpsqrt  15648  rpelogb  15675  2logb9irrALT  15700  binom4  15705  1sgmprm  15720  lgslem1  15731  lgsdir2lem1  15759  lgsdir2lem2  15760  lgsdir2lem3  15761  lgsdir2lem5  15763  lgs1  15775  gausslemma2dlem1a  15789  gausslemma2dlem3  15794  gausslemma2dlem4  15795  gausslemma2d  15800  lgseisenlem1  15801  lgseisenlem3  15803  lgsquadlem1  15808  lgsquadlem2  15809  lgsquad2lem2  15813  m1lgs  15816  2lgslem1a2  15818  2sqlem8  15854  setsiedg  15905  vdegp1cid  16169  clwwlknonex2lem1  16290  ex-exp  16326  ex-bc  16328  ex-gcd  16330  cvgcmp2nlemabs  16639  gfsumcl  16690