Theorem oveq1i 5953

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

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

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

Proof of Theorem oveq1i

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

Syntax hints:   = wceq 1372  (class class class)co 5943

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278  df-ov 5946

This theorem is referenced by:  caov12  6134  map1  6903  exmidpw2en  7008  halfnqq  7522  prarloclem5  7612  m1m1sr  7873  caucvgsrlemfv  7903  caucvgsr  7914  pitonnlem1  7957  axi2m1  7987  axcnre  7993  axcaucvg  8012  mvrraddi  8288  mvlladdi  8289  negsubdi  8327  mul02  8458  mulneg1  8466  mulreim  8676  recextlem1  8723  recdivap  8790  2p2e4  9162  2times  9163  3p2e5  9177  3p3e6  9178  4p2e6  9179  4p3e7  9180  4p4e8  9181  5p2e7  9182  5p3e8  9183  5p4e9  9184  6p2e8  9185  6p3e9  9186  7p2e9  9187  1mhlfehlf  9254  8th4div3  9255  halfpm6th  9256  nneoor  9474  9p1e10  9505  dfdec10  9506  num0h  9514  numsuc  9516  dec10p  9545  numma  9546  nummac  9547  numma2c  9548  numadd  9549  numaddc  9550  nummul2c  9552  decaddci  9563  decsubi  9565  decmul1  9566  5p5e10  9573  6p4e10  9574  7p3e10  9577  8p2e10  9582  decbin0  9642  decbin2  9643  elfzp1b  10218  elfzm1b  10219  fz01or  10232  fz1ssfz0  10238  fz0to4untppr  10245  qbtwnrelemcalc  10396  fldiv4p1lem1div2  10446  1tonninf  10584  mulexpzap  10722  expaddzap  10726  sq4e2t8  10780  cu2  10781  i3  10784  iexpcyc  10787  binom2i  10791  binom3  10800  3dec  10857  faclbnd  10884  bcm1k  10903  bcp1nk  10905  bcpasc  10909  hashp1i  10953  hashxp  10969  ccatlid  11060  imre  11133  crim  11140  remullem  11153  resqrexlemfp1  11291  resqrexlemover  11292  resqrexlemcalc1  11296  resqrexlemnm  11300  absexpzap  11362  absimle  11366  amgm2  11400  maxabslemlub  11489  fsumconst  11736  modfsummod  11740  binomlem  11765  binom11  11768  arisum  11780  arisum2  11781  georeclim  11795  geo2sum  11796  mertenslemi1  11817  mertenslem2  11818  mertensabs  11819  prodfrecap  11828  fprodm1s  11883  fprodp1s  11884  fprodrec  11911  fprodmodd  11923  efzval  11965  resinval  11997  recosval  11998  efi4p  11999  tan0  12013  efival  12014  cosadd  12019  cos2tsin  12033  ef01bndlem  12038  cos1bnd  12041  cos2bnd  12042  absefib  12053  efieq1re  12054  demoivreALT  12056  eirraplem  12059  3dvds  12146  3dvdsdec  12147  3dvds2dec  12148  odd2np1  12155  nn0o1gt2  12187  nn0o  12189  5ndvds3  12216  5ndvds6  12217  flodddiv4  12218  m1bits  12242  algrp1  12339  3lcm2e6woprm  12379  nn0gcdsq  12493  phiprmpw  12515  prmdiv  12528  prmdiveq  12529  pythagtriplem1  12559  pythagtriplem12  12569  pythagtriplem14  12571  pockthi  12652  infpnlem1  12653  4sqlem12  12696  4sqlem13m  12697  4sqlem19  12703  dec5dvds  12706  dec5nprm  12708  dec2nprm  12709  modxai  12710  modxp1i  12712  modsubi  12713  gcdmodi  12715  decsplit0b  12720  decsplit1  12722  decsplit  12723  karatsuba  12724  2exp7  12728  2exp8  12729  3exp3  12732  pwsbas  13095  subsubm  13286  mulg2  13438  subsubg  13504  unitsubm  13852  subsubrng  13947  subsubrg  13978  lsslss  14114  expghmap  14340  cnmpt1res  14739  rerestcntop  15001  rerest  15003  dvfvalap  15124  dvcnp2cntop  15142  dveflem  15169  plyun0  15179  dvply1  15208  reeff1oleme  15215  sin0pilem1  15224  sinhalfpilem  15234  cospi  15243  eulerid  15245  cos2pi  15247  ef2kpi  15249  sinhalfpip  15263  sinhalfpim  15264  coshalfpip  15265  coshalfpim  15266  sincosq3sgn  15271  sincosq4sgn  15272  cosq23lt0  15276  tangtx  15281  sincos4thpi  15283  sincos6thpi  15285  cosq34lt1  15293  rplogb1  15391  2logb9irr  15414  sqrt2cxp2logb9e3  15418  2logb9irrap  15420  binom4  15422  lgsdir2lem1  15476  lgsdir2lem2  15477  lgsdir2lem4  15479  lgsdir2lem5  15480  lgsne0  15486  1lgs  15491  gausslemma2dlem0e  15501  gausslemma2dlem0f  15502  gausslemma2dlem3  15511  gausslemma2d  15517  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem3  15520  lgseisenlem4  15521  lgseisen  15522  lgsquadlem1  15525  lgsquadlem2  15526  lgsquad2lem1  15529  lgsquad2lem2  15530  m1lgs  15533  2lgslem3a  15541  2lgslem3b  15542  2lgslem3c  15543  2lgslem3d  15544  2lgsoddprmlem3a  15555  2lgsoddprmlem3b  15556  2lgsoddprmlem3c  15557  2lgsoddprmlem3d  15558  ex-fl  15623  ex-exp  15625  ex-bc  15627  012of  15892  2o01f  15893  qdencn  15928  isomninnlem  15931  iswomninnlem  15950  ismkvnnlem  15953