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

Theorem oveq1i 5752
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
Hypothesis
Ref Expression
oveq1i.1  |-  A  =  B
Assertion
Ref Expression
oveq1i  |-  ( A F C )  =  ( B F C )

Proof of Theorem oveq1i
StepHypRef Expression
1 oveq1i.1 . 2  |-  A  =  B
2 oveq1 5749 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
31, 2ax-mp 5 1  |-  ( A F C )  =  ( B F C )
Colors of variables: wff set class
Syntax hints:    = wceq 1316  (class class class)co 5742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-iota 5058  df-fv 5101  df-ov 5745
This theorem is referenced by:  caov12  5927  map1  6674  halfnqq  7186  prarloclem5  7276  m1m1sr  7537  caucvgsrlemfv  7567  caucvgsr  7578  pitonnlem1  7621  axi2m1  7651  axcnre  7657  axcaucvg  7676  mvrraddi  7947  mvlladdi  7948  negsubdi  7986  mul02  8117  mulneg1  8125  mulreim  8334  recextlem1  8380  recdivap  8446  2p2e4  8815  2times  8816  3p2e5  8829  3p3e6  8830  4p2e6  8831  4p3e7  8832  4p4e8  8833  5p2e7  8834  5p3e8  8835  5p4e9  8836  6p2e8  8837  6p3e9  8838  7p2e9  8839  1mhlfehlf  8906  8th4div3  8907  halfpm6th  8908  nneoor  9121  9p1e10  9152  dfdec10  9153  num0h  9161  numsuc  9163  dec10p  9192  numma  9193  nummac  9194  numma2c  9195  numadd  9196  numaddc  9197  nummul2c  9199  decaddci  9210  decsubi  9212  decmul1  9213  5p5e10  9220  6p4e10  9221  7p3e10  9224  8p2e10  9229  decbin0  9289  decbin2  9290  elfzp1b  9845  elfzm1b  9846  fz01or  9859  fz1ssfz0  9865  qbtwnrelemcalc  10001  fldiv4p1lem1div2  10046  1tonninf  10181  mulexpzap  10301  expaddzap  10305  sq4e2t8  10358  cu2  10359  i3  10362  iexpcyc  10365  binom2i  10369  binom3  10377  3dec  10429  faclbnd  10455  bcm1k  10474  bcp1nk  10476  bcpasc  10480  hashp1i  10524  hashxp  10540  imre  10591  crim  10598  remullem  10611  resqrexlemfp1  10749  resqrexlemover  10750  resqrexlemcalc1  10754  resqrexlemnm  10758  absexpzap  10820  absimle  10824  amgm2  10858  maxabslemlub  10947  fsumconst  11191  modfsummod  11195  binomlem  11220  binom11  11223  arisum  11235  arisum2  11236  georeclim  11250  geo2sum  11251  mertenslemi1  11272  mertenslem2  11273  mertensabs  11274  efzval  11316  resinval  11349  recosval  11350  efi4p  11351  tan0  11365  efival  11366  cosadd  11371  cos2tsin  11385  ef01bndlem  11390  cos1bnd  11393  cos2bnd  11394  absefib  11404  efieq1re  11405  demoivreALT  11407  eirraplem  11410  3dvdsdec  11489  3dvds2dec  11490  odd2np1  11497  nn0o1gt2  11529  nn0o  11531  flodddiv4  11558  algrp1  11654  3lcm2e6woprm  11694  nn0gcdsq  11805  phiprmpw  11825  cnmpt1res  12392  rerestcntop  12646  dvfvalap  12746  dvcnp2cntop  12759  dveflem  12782  sin0pilem1  12789  sinhalfpilem  12799  cospi  12808  eulerid  12810  cos2pi  12812  ef2kpi  12814  sinhalfpip  12828  sinhalfpim  12829  coshalfpip  12830  coshalfpim  12831  sincosq3sgn  12836  sincosq4sgn  12837  cosq23lt0  12841  tangtx  12846  sincos4thpi  12848  sincos6thpi  12850  cosq34lt1  12858  ex-fl  12864  ex-exp  12866  ex-bc  12868  qdencn  13149  isomninnlem  13152
  Copyright terms: Public domain W3C validator