Theorem oveq2i 5886

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 5883	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Syntax hints:   = wceq 1353  (class class class)co 5875

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878

This theorem is referenced by:  caov32  6062  oa1suc  6468  nnm1  6526  nnm2  6527  mapsnconst  6694  mapsncnv  6695  mulidnq  7388  halfnqq  7409  addpinq1  7463  addnqpr1  7561  caucvgprlemm  7667  caucvgprprlemval  7687  caucvgprprlemnbj  7692  caucvgprprlemmu  7694  caucvgprprlemaddq  7707  caucvgprprlem1  7708  caucvgprprlem2  7709  m1p1sr  7759  m1m1sr  7760  0idsr  7766  1idsr  7767  00sr  7768  pn0sr  7770  ltm1sr  7776  caucvgsrlemoffres  7799  caucvgsr  7801  mulresr  7837  pitonnlem2  7846  axi2m1  7874  ax1rid  7876  axcnre  7880  add42i  8123  negid  8204  negsub  8205  subneg  8206  negsubdii  8242  apreap  8544  recexaplem2  8609  muleqadd  8625  crap0  8915  2p2e4  9046  3p2e5  9060  3p3e6  9061  4p2e6  9062  4p3e7  9063  4p4e8  9064  5p2e7  9065  5p3e8  9066  5p4e9  9067  6p2e8  9068  6p3e9  9069  7p2e9  9070  3t3e9  9076  8th4div3  9138  halfpm6th  9139  iap0  9142  addltmul  9155  div4p1lem1div2  9172  peano2z  9289  nn0n0n1ge2  9323  nneoor  9355  zeo  9358  numsuc  9397  numltc  9409  numsucc  9423  numma  9427  nummul1c  9432  decrmac  9441  decsubi  9446  decmul1  9447  decmul10add  9452  6p5lem  9453  5p5e10  9454  6p4e10  9455  7p3e10  9458  8p2e10  9463  4t3lem  9480  9t11e99  9513  decbin2  9524  fztp  10078  fzprval  10082  fztpval  10083  fzshftral  10108  fz0tp  10122  fz0to3un2pr  10123  fzo01  10216  fzo12sn  10217  fzo0to2pr  10218  fzo0to3tp  10219  fzo0to42pr  10220  intqfrac2  10319  intfracq  10320  sqval  10578  sq4e2t8  10618  cu2  10619  i3  10622  i4  10623  binom2i  10629  binom3  10638  3dec  10694  faclbnd  10721  faclbnd2  10722  bcn1  10738  bcn2  10744  4bc3eq4  10753  4bc2eq6  10754  reim0  10870  cji  10911  resqrexlemover  11019  resqrexlemcalc1  11023  resqrexlemcalc3  11025  absi  11068  fsump1i  11441  fsumconst  11462  modfsummodlemstep  11465  arisum2  11507  geoihalfsum  11530  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  fprodconst  11628  fprodrec  11637  ef0lem  11668  ege2le3  11679  eft0val  11701  ef4p  11702  efgt1p2  11703  efgt1p  11704  tanval2ap  11721  efival  11740  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  cos1bnd  11767  cos2bnd  11768  3dvdsdec  11870  3dvds2dec  11871  odd2np1lem  11877  odd2np1  11878  oddp1even  11881  mod2eq1n2dvds  11884  opoe  11900  6gcd4e2  11996  lcmneg  12074  3lcm2e6woprm  12086  6lcm4e12  12087  3prm  12128  3lcm2e6  12160  sqrt2irrlem  12161  pw2dvdslemn  12165  phiprm  12223  prmdiv  12235  pythagtriplem12  12275  pythagtriplem14  12277  pcfac  12348  prmpwdvds  12353  pockthi  12356  4sqlem5  12380  ressval2  12526  restin  13679  uptx  13777  cnrehmeocntop  14096  dvexp  14178  dvmptidcn  14181  dvmptccn  14182  dveflem  14190  sinhalfpilem  14215  efhalfpi  14223  cospi  14224  efipi  14225  sin2pi  14227  cos2pi  14228  ef2pi  14229  sin2pim  14237  cos2pim  14238  sinmpi  14239  cosmpi  14240  sinppi  14241  cosppi  14242  sincosq4sgn  14253  tangtx  14262  sincos4thpi  14264  sincos6thpi  14266  sincos3rdpi  14267  abssinper  14270  cosq34lt1  14274  1cxp  14324  ecxp  14325  rpcxpsqrt  14345  rpelogb  14370  2logb9irrALT  14395  binom4  14400  lgslem1  14404  lgsdir2lem1  14432  lgsdir2lem2  14433  lgsdir2lem3  14434  lgsdir2lem5  14436  lgs1  14448  lgseisenlem1  14453  m1lgs  14455  2sqlem8  14473  ex-exp  14482  ex-bc  14484  ex-gcd  14486  cvgcmp2nlemabs  14783