Theorem oveq1i 6060

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

Syntax hints:   = wceq 1398  (class class class)co 6050

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053

This theorem is referenced by:  caov12  6243  map1  7054  exmidpw2en  7172  halfnqq  7725  prarloclem5  7815  m1m1sr  8076  caucvgsrlemfv  8106  caucvgsr  8117  pitonnlem1  8160  axi2m1  8190  axcnre  8196  axcaucvg  8215  mvrraddi  8490  mvlladdi  8491  negsubdi  8529  mul02  8660  mulneg1  8668  mulreim  8878  recextlem1  8925  recdivap  8992  2p2e4  9364  2times  9365  3p2e5  9379  3p3e6  9380  4p2e6  9381  4p3e7  9382  4p4e8  9383  5p2e7  9384  5p3e8  9385  5p4e9  9386  6p2e8  9387  6p3e9  9388  7p2e9  9389  1mhlfehlf  9456  8th4div3  9457  halfpm6th  9458  nneoor  9680  9p1e10  9711  dfdec10  9712  num0h  9720  numsuc  9722  dec10p  9751  numma  9752  nummac  9753  numma2c  9754  numadd  9755  numaddc  9756  nummul2c  9758  decaddci  9769  decsubi  9771  decmul1  9772  5p5e10  9779  6p4e10  9780  7p3e10  9783  8p2e10  9788  decbin0  9848  decbin2  9849  elfzp1b  10431  elfzm1b  10432  fz01or  10445  fz1ssfz0  10451  fz0to4untppr  10458  qbtwnrelemcalc  10615  fldiv4p1lem1div2  10665  1tonninf  10803  mulexpzap  10941  expaddzap  10945  sq4e2t8  10999  cu2  11000  i3  11003  iexpcyc  11006  binom2i  11010  binom3  11019  3dec  11076  faclbnd  11103  bcm1k  11122  bcp1nk  11124  bcpasc  11128  hashp1i  11175  hashxp  11191  hashpwfi  11193  hashfibc  11207  ccatlid  11294  pfxccatin12lem2c  11422  imre  11536  crim  11543  remullem  11556  resqrexlemfp1  11694  resqrexlemover  11695  resqrexlemcalc1  11699  resqrexlemnm  11703  absexpzap  11765  absimle  11769  amgm2  11803  maxabslemlub  11892  fsumconst  12140  modfsummod  12144  binomlem  12169  binom11  12172  arisum  12184  arisum2  12185  georeclim  12199  geo2sum  12200  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  prodfrecap  12232  fprodm1s  12287  fprodp1s  12288  fprodrec  12315  fprodmodd  12327  efzval  12369  resinval  12401  recosval  12402  efi4p  12403  tan0  12417  efival  12418  cosadd  12423  cos2tsin  12437  ef01bndlem  12442  cos1bnd  12445  cos2bnd  12446  absefib  12457  efieq1re  12458  demoivreALT  12460  eirraplem  12463  3dvds  12550  3dvdsdec  12551  3dvds2dec  12552  odd2np1  12559  nn0o1gt2  12591  nn0o  12593  5ndvds3  12620  5ndvds6  12621  flodddiv4  12622  m1bits  12646  algrp1  12743  3lcm2e6woprm  12783  nn0gcdsq  12897  phiprmpw  12919  prmdiv  12932  prmdiveq  12933  pythagtriplem1  12963  pythagtriplem12  12973  pythagtriplem14  12975  pockthi  13056  infpnlem1  13057  4sqlem12  13100  4sqlem13m  13101  4sqlem19  13107  dec5dvds  13110  dec5nprm  13112  dec2nprm  13113  modxai  13114  modxp1i  13116  modsubi  13117  gcdmodi  13119  decsplit0b  13124  decsplit1  13126  decsplit  13127  karatsuba  13128  2exp7  13132  2exp8  13133  3exp3  13136  ballotfilem1  13139  ballotfilem2  13142  pwsbas  13505  subsubm  13696  mulg2  13848  subsubg  13914  unitsubm  14264  subsubrng  14359  subsubrg  14390  lsslss  14529  expghmap  14755  cnmpt1res  15161  rerestcntop  15423  rerest  15425  dvfvalap  15546  dvcnp2cntop  15564  dveflem  15591  plyun0  15601  dvply1  15630  reeff1oleme  15637  sin0pilem1  15646  sinhalfpilem  15656  cospi  15665  eulerid  15667  cos2pi  15669  ef2kpi  15671  sinhalfpip  15685  sinhalfpim  15686  coshalfpip  15687  coshalfpim  15688  sincosq3sgn  15693  sincosq4sgn  15694  cosq23lt0  15698  tangtx  15703  sincos4thpi  15705  sincos6thpi  15707  cosq34lt1  15715  rplogb1  15813  2logb9irr  15836  sqrt2cxp2logb9e3  15840  2logb9irrap  15842  binom4  15844  lgsdir2lem1  15901  lgsdir2lem2  15902  lgsdir2lem4  15904  lgsdir2lem5  15905  lgsne0  15911  1lgs  15916  gausslemma2dlem0e  15926  gausslemma2dlem0f  15927  gausslemma2dlem3  15936  gausslemma2d  15942  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem1  15954  lgsquad2lem2  15955  m1lgs  15958  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2lgsoddprmlem3a  15980  2lgsoddprmlem3b  15981  2lgsoddprmlem3c  15982  2lgsoddprmlem3d  15983  ex-fl  16493  ex-exp  16495  ex-bc  16497  depindlem1  16501  012of  16767  2o01f  16768  qdencn  16807  isomninnlem  16814  iswomninnlem  16834  ismkvnnlem  16837