Theorem oveq1i 5885

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

Syntax hints:   = wceq 1353  (class class class)co 5875

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878

This theorem is referenced by:  caov12  6063  map1  6812  halfnqq  7409  prarloclem5  7499  m1m1sr  7760  caucvgsrlemfv  7790  caucvgsr  7801  pitonnlem1  7844  axi2m1  7874  axcnre  7880  axcaucvg  7899  mvrraddi  8174  mvlladdi  8175  negsubdi  8213  mul02  8344  mulneg1  8352  mulreim  8561  recextlem1  8608  recdivap  8675  2p2e4  9046  2times  9047  3p2e5  9060  3p3e6  9061  4p2e6  9062  4p3e7  9063  4p4e8  9064  5p2e7  9065  5p3e8  9066  5p4e9  9067  6p2e8  9068  6p3e9  9069  7p2e9  9070  1mhlfehlf  9137  8th4div3  9138  halfpm6th  9139  nneoor  9355  9p1e10  9386  dfdec10  9387  num0h  9395  numsuc  9397  dec10p  9426  numma  9427  nummac  9428  numma2c  9429  numadd  9430  numaddc  9431  nummul2c  9433  decaddci  9444  decsubi  9446  decmul1  9447  5p5e10  9454  6p4e10  9455  7p3e10  9458  8p2e10  9463  decbin0  9523  decbin2  9524  elfzp1b  10097  elfzm1b  10098  fz01or  10111  fz1ssfz0  10117  fz0to4untppr  10124  qbtwnrelemcalc  10256  fldiv4p1lem1div2  10305  1tonninf  10440  mulexpzap  10560  expaddzap  10564  sq4e2t8  10618  cu2  10619  i3  10622  iexpcyc  10625  binom2i  10629  binom3  10638  3dec  10694  faclbnd  10721  bcm1k  10740  bcp1nk  10742  bcpasc  10746  hashp1i  10790  hashxp  10806  imre  10860  crim  10867  remullem  10880  resqrexlemfp1  11018  resqrexlemover  11019  resqrexlemcalc1  11023  resqrexlemnm  11027  absexpzap  11089  absimle  11093  amgm2  11127  maxabslemlub  11216  fsumconst  11462  modfsummod  11466  binomlem  11491  binom11  11494  arisum  11506  arisum2  11507  georeclim  11521  geo2sum  11522  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodfrecap  11554  fprodm1s  11609  fprodp1s  11610  fprodrec  11637  fprodmodd  11649  efzval  11691  resinval  11723  recosval  11724  efi4p  11725  tan0  11739  efival  11740  cosadd  11745  cos2tsin  11759  ef01bndlem  11764  cos1bnd  11767  cos2bnd  11768  absefib  11778  efieq1re  11779  demoivreALT  11781  eirraplem  11784  3dvdsdec  11870  3dvds2dec  11871  odd2np1  11878  nn0o1gt2  11910  nn0o  11912  flodddiv4  11939  algrp1  12046  3lcm2e6woprm  12086  nn0gcdsq  12200  phiprmpw  12222  prmdiv  12235  prmdiveq  12236  pythagtriplem1  12265  pythagtriplem12  12275  pythagtriplem14  12277  pockthi  12356  infpnlem1  12357  mulg2  12992  subsubg  13057  unitsubm  13288  subsubrg  13366  cnmpt1res  13799  rerestcntop  14053  dvfvalap  14153  dvcnp2cntop  14166  dveflem  14190  reeff1oleme  14196  sin0pilem1  14205  sinhalfpilem  14215  cospi  14224  eulerid  14226  cos2pi  14228  ef2kpi  14230  sinhalfpip  14244  sinhalfpim  14245  coshalfpip  14246  coshalfpim  14247  sincosq3sgn  14252  sincosq4sgn  14253  cosq23lt0  14257  tangtx  14262  sincos4thpi  14264  sincos6thpi  14266  cosq34lt1  14274  rplogb1  14369  2logb9irr  14392  sqrt2cxp2logb9e3  14396  2logb9irrap  14398  binom4  14400  lgsdir2lem1  14432  lgsdir2lem2  14433  lgsdir2lem4  14435  lgsdir2lem5  14436  lgsne0  14442  1lgs  14447  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2lgsoddprmlem3a  14458  2lgsoddprmlem3b  14459  2lgsoddprmlem3c  14460  2lgsoddprmlem3d  14461  ex-fl  14480  ex-exp  14482  ex-bc  14484  012of  14748  2o01f  14749  qdencn  14778  isomninnlem  14781  iswomninnlem  14800  ismkvnnlem  14803