Theorem oveq1i 5977

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

Syntax hints:   = wceq 1373  (class class class)co 5967

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970

This theorem is referenced by:  caov12  6158  map1  6928  exmidpw2en  7035  halfnqq  7558  prarloclem5  7648  m1m1sr  7909  caucvgsrlemfv  7939  caucvgsr  7950  pitonnlem1  7993  axi2m1  8023  axcnre  8029  axcaucvg  8048  mvrraddi  8324  mvlladdi  8325  negsubdi  8363  mul02  8494  mulneg1  8502  mulreim  8712  recextlem1  8759  recdivap  8826  2p2e4  9198  2times  9199  3p2e5  9213  3p3e6  9214  4p2e6  9215  4p3e7  9216  4p4e8  9217  5p2e7  9218  5p3e8  9219  5p4e9  9220  6p2e8  9221  6p3e9  9222  7p2e9  9223  1mhlfehlf  9290  8th4div3  9291  halfpm6th  9292  nneoor  9510  9p1e10  9541  dfdec10  9542  num0h  9550  numsuc  9552  dec10p  9581  numma  9582  nummac  9583  numma2c  9584  numadd  9585  numaddc  9586  nummul2c  9588  decaddci  9599  decsubi  9601  decmul1  9602  5p5e10  9609  6p4e10  9610  7p3e10  9613  8p2e10  9618  decbin0  9678  decbin2  9679  elfzp1b  10254  elfzm1b  10255  fz01or  10268  fz1ssfz0  10274  fz0to4untppr  10281  qbtwnrelemcalc  10435  fldiv4p1lem1div2  10485  1tonninf  10623  mulexpzap  10761  expaddzap  10765  sq4e2t8  10819  cu2  10820  i3  10823  iexpcyc  10826  binom2i  10830  binom3  10839  3dec  10896  faclbnd  10923  bcm1k  10942  bcp1nk  10944  bcpasc  10948  hashp1i  10992  hashxp  11008  ccatlid  11100  pfxccatin12lem2c  11221  imre  11277  crim  11284  remullem  11297  resqrexlemfp1  11435  resqrexlemover  11436  resqrexlemcalc1  11440  resqrexlemnm  11444  absexpzap  11506  absimle  11510  amgm2  11544  maxabslemlub  11633  fsumconst  11880  modfsummod  11884  binomlem  11909  binom11  11912  arisum  11924  arisum2  11925  georeclim  11939  geo2sum  11940  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  prodfrecap  11972  fprodm1s  12027  fprodp1s  12028  fprodrec  12055  fprodmodd  12067  efzval  12109  resinval  12141  recosval  12142  efi4p  12143  tan0  12157  efival  12158  cosadd  12163  cos2tsin  12177  ef01bndlem  12182  cos1bnd  12185  cos2bnd  12186  absefib  12197  efieq1re  12198  demoivreALT  12200  eirraplem  12203  3dvds  12290  3dvdsdec  12291  3dvds2dec  12292  odd2np1  12299  nn0o1gt2  12331  nn0o  12333  5ndvds3  12360  5ndvds6  12361  flodddiv4  12362  m1bits  12386  algrp1  12483  3lcm2e6woprm  12523  nn0gcdsq  12637  phiprmpw  12659  prmdiv  12672  prmdiveq  12673  pythagtriplem1  12703  pythagtriplem12  12713  pythagtriplem14  12715  pockthi  12796  infpnlem1  12797  4sqlem12  12840  4sqlem13m  12841  4sqlem19  12847  dec5dvds  12850  dec5nprm  12852  dec2nprm  12853  modxai  12854  modxp1i  12856  modsubi  12857  gcdmodi  12859  decsplit0b  12864  decsplit1  12866  decsplit  12867  karatsuba  12868  2exp7  12872  2exp8  12873  3exp3  12876  pwsbas  13239  subsubm  13430  mulg2  13582  subsubg  13648  unitsubm  13996  subsubrng  14091  subsubrg  14122  lsslss  14258  expghmap  14484  cnmpt1res  14883  rerestcntop  15145  rerest  15147  dvfvalap  15268  dvcnp2cntop  15286  dveflem  15313  plyun0  15323  dvply1  15352  reeff1oleme  15359  sin0pilem1  15368  sinhalfpilem  15378  cospi  15387  eulerid  15389  cos2pi  15391  ef2kpi  15393  sinhalfpip  15407  sinhalfpim  15408  coshalfpip  15409  coshalfpim  15410  sincosq3sgn  15415  sincosq4sgn  15416  cosq23lt0  15420  tangtx  15425  sincos4thpi  15427  sincos6thpi  15429  cosq34lt1  15437  rplogb1  15535  2logb9irr  15558  sqrt2cxp2logb9e3  15562  2logb9irrap  15564  binom4  15566  lgsdir2lem1  15620  lgsdir2lem2  15621  lgsdir2lem4  15623  lgsdir2lem5  15624  lgsne0  15630  1lgs  15635  gausslemma2dlem0e  15645  gausslemma2dlem0f  15646  gausslemma2dlem3  15655  gausslemma2d  15661  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgseisen  15666  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem1  15673  lgsquad2lem2  15674  m1lgs  15677  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgsoddprmlem3a  15699  2lgsoddprmlem3b  15700  2lgsoddprmlem3c  15701  2lgsoddprmlem3d  15702  ex-fl  15861  ex-exp  15863  ex-bc  15865  012of  16130  2o01f  16131  qdencn  16168  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193