Theorem oveq1i 6068

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  caov12  6251  map1  7067  exmidpw2en  7185  halfnqq  7741  prarloclem5  7831  m1m1sr  8092  caucvgsrlemfv  8122  caucvgsr  8133  pitonnlem1  8176  axi2m1  8206  axcnre  8212  axcaucvg  8231  mvrraddi  8506  mvlladdi  8507  negsubdi  8545  mul02  8677  mulneg1  8685  mulreim  8895  recextlem1  8942  recdivap  9009  2p2e4  9381  2times  9382  3p2e5  9396  3p3e6  9397  4p2e6  9398  4p3e7  9399  4p4e8  9400  5p2e7  9401  5p3e8  9402  5p4e9  9403  6p2e8  9404  6p3e9  9405  7p2e9  9406  1mhlfehlf  9473  8th4div3  9474  halfpm6th  9475  nneoor  9698  9p1e10  9729  dfdec10  9730  num0h  9738  numsuc  9740  dec10p  9769  numma  9770  nummac  9771  numma2c  9772  numadd  9773  numaddc  9774  nummul2c  9776  decaddci  9787  decsubi  9789  decmul1  9790  5p5e10  9797  6p4e10  9798  7p3e10  9801  8p2e10  9806  decbin0  9866  decbin2  9867  elfzp1b  10453  elfzm1b  10454  fz01or  10467  fz1ssfz0  10473  fz0to4untppr  10480  qbtwnrelemcalc  10639  fldiv4p1lem1div2  10689  1tonninf  10827  mulexpzap  10965  expaddzap  10969  sq4e2t8  11023  cu2  11024  i3  11027  iexpcyc  11030  binom2i  11034  binom3  11043  3dec  11101  faclbnd  11128  bcm1k  11147  bcp1nk  11149  bcpasc  11153  hashp1i  11200  hashxp  11216  hashpwfi  11218  hashfibc  11232  ccatlid  11319  pfxccatin12lem2c  11447  imre  11561  crim  11568  remullem  11581  resqrexlemfp1  11719  resqrexlemover  11720  resqrexlemcalc1  11724  resqrexlemnm  11728  absexpzap  11790  absimle  11794  amgm2  11828  maxabslemlub  11917  fsumconst  12165  modfsummod  12169  binomlem  12194  binom11  12197  arisum  12209  arisum2  12210  georeclim  12224  geo2sum  12225  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  prodfrecap  12257  fprodm1s  12312  fprodp1s  12313  fprodrec  12340  fprodmodd  12352  efzval  12394  resinval  12426  recosval  12427  efi4p  12428  tan0  12442  efival  12443  cosadd  12448  cos2tsin  12462  ef01bndlem  12467  cos1bnd  12470  cos2bnd  12471  absefib  12482  efieq1re  12483  demoivreALT  12485  eirraplem  12488  3dvds  12575  3dvdsdec  12576  3dvds2dec  12577  odd2np1  12584  nn0o1gt2  12616  nn0o  12618  5ndvds3  12645  5ndvds6  12646  flodddiv4  12647  m1bits  12671  algrp1  12768  3lcm2e6woprm  12808  nn0gcdsq  12922  phiprmpw  12944  prmdiv  12957  prmdiveq  12958  pythagtriplem1  12988  pythagtriplem12  12998  pythagtriplem14  13000  pockthi  13081  infpnlem1  13082  4sqlem12  13125  4sqlem13m  13126  4sqlem19  13132  dec5dvds  13135  dec5nprm  13137  dec2nprm  13138  modxai  13139  modxp1i  13141  modsubi  13142  gcdmodi  13144  decsplit0b  13149  decsplit1  13151  decsplit  13152  karatsuba  13153  2exp7  13157  2exp8  13158  3exp3  13161  ballotfilem1  13164  ballotfilem2  13172  ballotfilemi1  13189  ballotfilemii  13190  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemfrceq  13216  ballotfilemth  13225  subsubm  13738  mulg2  13884  subsubg  13950  pwsbas  14147  unitsubm  14364  subsubrng  14460  subsubrg  14491  lsslss  14655  expghmap  14881  cnmpt1res  15287  rerestcntop  15549  rerest  15551  dvfvalap  15672  dvcnp2cntop  15690  dveflem  15717  plyun0  15727  dvply1  15756  reeff1oleme  15763  sin0pilem1  15772  sinhalfpilem  15782  cospi  15791  eulerid  15793  cos2pi  15795  ef2kpi  15797  sinhalfpip  15811  sinhalfpim  15812  coshalfpip  15813  coshalfpim  15814  sincosq3sgn  15819  sincosq4sgn  15820  cosq23lt0  15824  tangtx  15829  sincos4thpi  15831  sincos6thpi  15833  cosq34lt1  15841  rplogb1  15939  2logb9irr  15962  sqrt2cxp2logb9e3  15966  2logb9irrap  15968  binom4  15970  lgsdir2lem1  16027  lgsdir2lem2  16028  lgsdir2lem4  16030  lgsdir2lem5  16031  lgsne0  16037  1lgs  16042  gausslemma2dlem0e  16052  gausslemma2dlem0f  16053  gausslemma2dlem3  16062  gausslemma2d  16068  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgseisen  16073  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem1  16080  lgsquad2lem2  16081  m1lgs  16084  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgsoddprmlem3a  16106  2lgsoddprmlem3b  16107  2lgsoddprmlem3c  16108  2lgsoddprmlem3d  16109  ex-fl  16619  ex-exp  16621  ex-bc  16623  depindlem1  16627  012of  16893  2o01f  16894  qdencn  16933  isomninnlem  16940  iswomninnlem  16960  ismkvnnlem  16963