Theorem oveq1i 6069

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

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

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 3701  df-pr 3702  df-op 3704  df-uni 3921  df-br 4116  df-iota 5318  df-fv 5366  df-ov 6062

This theorem is referenced by:  caov12  6252  map1  7068  exmidpw2en  7186  halfnqq  7742  prarloclem5  7832  m1m1sr  8093  caucvgsrlemfv  8123  caucvgsr  8134  pitonnlem1  8177  axi2m1  8207  axcnre  8213  axcaucvg  8232  mvrraddi  8508  mvlladdi  8509  negsubdi  8547  mul02  8679  mulneg1  8687  mulreim  8897  recextlem1  8944  recdivap  9013  2p2e4  9385  2times  9386  3p2e5  9400  3p3e6  9401  4p2e6  9402  4p3e7  9403  4p4e8  9404  5p2e7  9405  5p3e8  9406  5p4e9  9407  6p2e8  9408  6p3e9  9409  7p2e9  9410  1mhlfehlf  9477  8th4div3  9478  halfpm6th  9479  nneoor  9702  9p1e10  9733  dfdec10  9734  num0h  9742  numsuc  9744  dec10p  9773  numma  9774  nummac  9775  numma2c  9776  numadd  9777  numaddc  9778  nummul2c  9780  decaddci  9791  decsubi  9793  decmul1  9794  5p5e10  9801  6p4e10  9802  7p3e10  9805  8p2e10  9810  decbin0  9870  decbin2  9871  elfzp1b  10457  elfzm1b  10458  fz01or  10471  fz1ssfz0  10477  fz0to4untppr  10484  qbtwnrelemcalc  10643  fldiv4p1lem1div2  10693  1tonninf  10831  mulexpzap  10969  expaddzap  10973  sq4e2t8  11027  cu2  11028  i3  11031  iexpcyc  11034  binom2i  11038  binom3  11047  3dec  11105  faclbnd  11132  bcm1k  11151  bcp1nk  11153  bcpasc  11157  hashp1i  11204  hashxp  11220  hashpwfi  11222  hashfibc  11236  ccatlid  11323  pfxccatin12lem2c  11451  imre  11565  crim  11572  remullem  11585  sq01  11609  resqrexlemfp1  11724  resqrexlemover  11725  resqrexlemcalc1  11729  resqrexlemnm  11733  absexpzap  11795  absimle  11799  amgm2  11833  maxabslemlub  11922  fsumconst  12170  modfsummod  12174  binomlem  12199  binom11  12202  arisum  12214  arisum2  12215  georeclim  12229  geo2sum  12230  mertenslemi1  12251  mertenslem2  12252  mertensabs  12253  prodfrecap  12262  fprodm1s  12317  fprodp1s  12318  fprodrec  12345  fprodmodd  12357  efzval  12399  resinval  12431  recosval  12432  efi4p  12433  tan0  12447  efival  12448  cosadd  12453  cos2tsin  12467  ef01bndlem  12472  cos1bnd  12475  cos2bnd  12476  absefib  12487  efieq1re  12488  demoivreALT  12490  eirraplem  12493  3dvds  12580  3dvdsdec  12581  3dvds2dec  12582  odd2np1  12589  nn0o1gt2  12621  nn0o  12623  5ndvds3  12650  5ndvds6  12651  flodddiv4  12652  m1bits  12676  algrp1  12773  3lcm2e6woprm  12813  nn0gcdsq  12927  phiprmpw  12949  prmdiv  12962  prmdiveq  12963  pythagtriplem1  12993  pythagtriplem12  13003  pythagtriplem14  13005  pockthi  13086  infpnlem1  13087  4sqlem12  13130  4sqlem13m  13131  4sqlem19  13137  dec5dvds  13140  dec5nprm  13142  dec2nprm  13143  modxai  13144  modxp1i  13146  modsubi  13147  gcdmodi  13149  decsplit0b  13154  decsplit1  13156  decsplit  13157  karatsuba  13158  2exp7  13162  2exp8  13163  3exp3  13166  ballotfilem1  13169  ballotfilem2  13177  ballotfilemi1  13194  ballotfilemii  13195  ballotfilemic  13199  ballotfilem1c  13200  ballotfilemfrceq  13221  ballotfilemth  13230  subsubm  13743  mulg2  13889  subsubg  13955  pwsbas  14152  unitsubm  14369  subsubrng  14465  subsubrg  14496  lsslss  14660  expghmap  14886  cnmpt1res  15292  rerestcntop  15554  rerest  15556  dvfvalap  15677  dvcnp2cntop  15695  dveflem  15722  plyun0  15732  dvply1  15761  reeff1oleme  15768  sin0pilem1  15777  sinhalfpilem  15787  cospi  15796  eulerid  15798  cos2pi  15800  ef2kpi  15802  sinhalfpip  15816  sinhalfpim  15817  coshalfpip  15818  coshalfpim  15819  sincosq3sgn  15824  sincosq4sgn  15825  cosq23lt0  15829  tangtx  15834  sincos4thpi  15836  sincos6thpi  15838  cosq34lt1  15846  rplogb1  15944  2logb9irr  15967  sqrt2cxp2logb9e3  15971  2logb9irrap  15973  binom4  15975  lgsdir2lem1  16032  lgsdir2lem2  16033  lgsdir2lem4  16035  lgsdir2lem5  16036  lgsne0  16042  1lgs  16047  gausslemma2dlem0e  16057  gausslemma2dlem0f  16058  gausslemma2dlem3  16067  gausslemma2d  16073  lgseisenlem1  16074  lgseisenlem2  16075  lgseisenlem3  16076  lgseisenlem4  16077  lgseisen  16078  lgsquadlem1  16081  lgsquadlem2  16082  lgsquad2lem1  16085  lgsquad2lem2  16086  m1lgs  16089  2lgslem3a  16097  2lgslem3b  16098  2lgslem3c  16099  2lgslem3d  16100  2lgsoddprmlem3a  16111  2lgsoddprmlem3b  16112  2lgsoddprmlem3c  16113  2lgsoddprmlem3d  16114  ex-fl  16624  ex-exp  16626  ex-bc  16628  depindlem1  16632  012of  16908  2o01f  16909  qdencn  16948  isomninnlem  16955  iswomninnlem  16975  ismkvnnlem  16978