ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  oveq1i GIF version

Theorem oveq1i 5879
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
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq1 5876 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2ax-mp 5 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Colors of variables: wff set class
Syntax hints:   = wceq 1353  (class class class)co 5869
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 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-iota 5174  df-fv 5220  df-ov 5872
This theorem is referenced by:  caov12  6057  map1  6806  halfnqq  7397  prarloclem5  7487  m1m1sr  7748  caucvgsrlemfv  7778  caucvgsr  7789  pitonnlem1  7832  axi2m1  7862  axcnre  7868  axcaucvg  7887  mvrraddi  8161  mvlladdi  8162  negsubdi  8200  mul02  8331  mulneg1  8339  mulreim  8548  recextlem1  8594  recdivap  8661  2p2e4  9032  2times  9033  3p2e5  9046  3p3e6  9047  4p2e6  9048  4p3e7  9049  4p4e8  9050  5p2e7  9051  5p3e8  9052  5p4e9  9053  6p2e8  9054  6p3e9  9055  7p2e9  9056  1mhlfehlf  9123  8th4div3  9124  halfpm6th  9125  nneoor  9341  9p1e10  9372  dfdec10  9373  num0h  9381  numsuc  9383  dec10p  9412  numma  9413  nummac  9414  numma2c  9415  numadd  9416  numaddc  9417  nummul2c  9419  decaddci  9430  decsubi  9432  decmul1  9433  5p5e10  9440  6p4e10  9441  7p3e10  9444  8p2e10  9449  decbin0  9509  decbin2  9510  elfzp1b  10080  elfzm1b  10081  fz01or  10094  fz1ssfz0  10100  fz0to4untppr  10107  qbtwnrelemcalc  10239  fldiv4p1lem1div2  10288  1tonninf  10423  mulexpzap  10543  expaddzap  10547  sq4e2t8  10600  cu2  10601  i3  10604  iexpcyc  10607  binom2i  10611  binom3  10620  3dec  10675  faclbnd  10702  bcm1k  10721  bcp1nk  10723  bcpasc  10727  hashp1i  10771  hashxp  10787  imre  10841  crim  10848  remullem  10861  resqrexlemfp1  10999  resqrexlemover  11000  resqrexlemcalc1  11004  resqrexlemnm  11008  absexpzap  11070  absimle  11074  amgm2  11108  maxabslemlub  11197  fsumconst  11443  modfsummod  11447  binomlem  11472  binom11  11475  arisum  11487  arisum2  11488  georeclim  11502  geo2sum  11503  mertenslemi1  11524  mertenslem2  11525  mertensabs  11526  prodfrecap  11535  fprodm1s  11590  fprodp1s  11591  fprodrec  11618  fprodmodd  11630  efzval  11672  resinval  11704  recosval  11705  efi4p  11706  tan0  11720  efival  11721  cosadd  11726  cos2tsin  11740  ef01bndlem  11745  cos1bnd  11748  cos2bnd  11749  absefib  11759  efieq1re  11760  demoivreALT  11762  eirraplem  11765  3dvdsdec  11850  3dvds2dec  11851  odd2np1  11858  nn0o1gt2  11890  nn0o  11892  flodddiv4  11919  algrp1  12026  3lcm2e6woprm  12066  nn0gcdsq  12180  phiprmpw  12202  prmdiv  12215  prmdiveq  12216  pythagtriplem1  12245  pythagtriplem12  12255  pythagtriplem14  12257  pockthi  12336  infpnlem1  12337  mulg2  12878  unitsubm  13110  cnmpt1res  13456  rerestcntop  13710  dvfvalap  13810  dvcnp2cntop  13823  dveflem  13847  reeff1oleme  13853  sin0pilem1  13862  sinhalfpilem  13872  cospi  13881  eulerid  13883  cos2pi  13885  ef2kpi  13887  sinhalfpip  13901  sinhalfpim  13902  coshalfpip  13903  coshalfpim  13904  sincosq3sgn  13909  sincosq4sgn  13910  cosq23lt0  13914  tangtx  13919  sincos4thpi  13921  sincos6thpi  13923  cosq34lt1  13931  rplogb1  14026  2logb9irr  14049  sqrt2cxp2logb9e3  14053  2logb9irrap  14055  binom4  14057  lgsdir2lem1  14089  lgsdir2lem2  14090  lgsdir2lem4  14092  lgsdir2lem5  14093  lgsne0  14099  1lgs  14104  ex-fl  14126  ex-exp  14128  ex-bc  14130  012of  14394  2o01f  14395  qdencn  14424  isomninnlem  14427  iswomninnlem  14446  ismkvnnlem  14449
  Copyright terms: Public domain W3C validator