Theorem oveq1i 6038

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  caov12  6221  map1  7030  exmidpw2en  7147  halfnqq  7673  prarloclem5  7763  m1m1sr  8024  caucvgsrlemfv  8054  caucvgsr  8065  pitonnlem1  8108  axi2m1  8138  axcnre  8144  axcaucvg  8163  mvrraddi  8438  mvlladdi  8439  negsubdi  8477  mul02  8608  mulneg1  8616  mulreim  8826  recextlem1  8873  recdivap  8940  2p2e4  9312  2times  9313  3p2e5  9327  3p3e6  9328  4p2e6  9329  4p3e7  9330  4p4e8  9331  5p2e7  9332  5p3e8  9333  5p4e9  9334  6p2e8  9335  6p3e9  9336  7p2e9  9337  1mhlfehlf  9404  8th4div3  9405  halfpm6th  9406  nneoor  9626  9p1e10  9657  dfdec10  9658  num0h  9666  numsuc  9668  dec10p  9697  numma  9698  nummac  9699  numma2c  9700  numadd  9701  numaddc  9702  nummul2c  9704  decaddci  9715  decsubi  9717  decmul1  9718  5p5e10  9725  6p4e10  9726  7p3e10  9729  8p2e10  9734  decbin0  9794  decbin2  9795  elfzp1b  10377  elfzm1b  10378  fz01or  10391  fz1ssfz0  10397  fz0to4untppr  10404  qbtwnrelemcalc  10561  fldiv4p1lem1div2  10611  1tonninf  10749  mulexpzap  10887  expaddzap  10891  sq4e2t8  10945  cu2  10946  i3  10949  iexpcyc  10952  binom2i  10956  binom3  10965  3dec  11022  faclbnd  11049  bcm1k  11068  bcp1nk  11070  bcpasc  11074  hashp1i  11120  hashxp  11136  ccatlid  11232  pfxccatin12lem2c  11360  imre  11474  crim  11481  remullem  11494  resqrexlemfp1  11632  resqrexlemover  11633  resqrexlemcalc1  11637  resqrexlemnm  11641  absexpzap  11703  absimle  11707  amgm2  11741  maxabslemlub  11830  fsumconst  12078  modfsummod  12082  binomlem  12107  binom11  12110  arisum  12122  arisum2  12123  georeclim  12137  geo2sum  12138  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  prodfrecap  12170  fprodm1s  12225  fprodp1s  12226  fprodrec  12253  fprodmodd  12265  efzval  12307  resinval  12339  recosval  12340  efi4p  12341  tan0  12355  efival  12356  cosadd  12361  cos2tsin  12375  ef01bndlem  12380  cos1bnd  12383  cos2bnd  12384  absefib  12395  efieq1re  12396  demoivreALT  12398  eirraplem  12401  3dvds  12488  3dvdsdec  12489  3dvds2dec  12490  odd2np1  12497  nn0o1gt2  12529  nn0o  12531  5ndvds3  12558  5ndvds6  12559  flodddiv4  12560  m1bits  12584  algrp1  12681  3lcm2e6woprm  12721  nn0gcdsq  12835  phiprmpw  12857  prmdiv  12870  prmdiveq  12871  pythagtriplem1  12901  pythagtriplem12  12911  pythagtriplem14  12913  pockthi  12994  infpnlem1  12995  4sqlem12  13038  4sqlem13m  13039  4sqlem19  13045  dec5dvds  13048  dec5nprm  13050  dec2nprm  13051  modxai  13052  modxp1i  13054  modsubi  13055  gcdmodi  13057  decsplit0b  13062  decsplit1  13064  decsplit  13065  karatsuba  13066  2exp7  13070  2exp8  13071  3exp3  13074  pwsbas  13438  subsubm  13629  mulg2  13781  subsubg  13847  unitsubm  14197  subsubrng  14292  subsubrg  14323  lsslss  14460  expghmap  14686  cnmpt1res  15090  rerestcntop  15352  rerest  15354  dvfvalap  15475  dvcnp2cntop  15493  dveflem  15520  plyun0  15530  dvply1  15559  reeff1oleme  15566  sin0pilem1  15575  sinhalfpilem  15585  cospi  15594  eulerid  15596  cos2pi  15598  ef2kpi  15600  sinhalfpip  15614  sinhalfpim  15615  coshalfpip  15616  coshalfpim  15617  sincosq3sgn  15622  sincosq4sgn  15623  cosq23lt0  15627  tangtx  15632  sincos4thpi  15634  sincos6thpi  15636  cosq34lt1  15644  rplogb1  15742  2logb9irr  15765  sqrt2cxp2logb9e3  15769  2logb9irrap  15771  binom4  15773  lgsdir2lem1  15830  lgsdir2lem2  15831  lgsdir2lem4  15833  lgsdir2lem5  15834  lgsne0  15840  1lgs  15845  gausslemma2dlem0e  15855  gausslemma2dlem0f  15856  gausslemma2dlem3  15865  gausslemma2d  15871  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgseisen  15876  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem1  15883  lgsquad2lem2  15884  m1lgs  15887  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2lgsoddprmlem3a  15909  2lgsoddprmlem3b  15910  2lgsoddprmlem3c  15911  2lgsoddprmlem3d  15912  ex-fl  16422  ex-exp  16424  ex-bc  16426  depindlem1  16430  012of  16696  2o01f  16697  qdencn  16738  isomninnlem  16745  iswomninnlem  16765  ismkvnnlem  16768