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

Theorem oveq1i 5750
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 5747 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2ax-mp 5 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Colors of variables: wff set class
Syntax hints:   = wceq 1314  (class class class)co 5740
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rex 2397  df-v 2660  df-un 3043  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-iota 5056  df-fv 5099  df-ov 5743
This theorem is referenced by:  caov12  5925  map1  6672  halfnqq  7182  prarloclem5  7272  m1m1sr  7533  caucvgsrlemfv  7563  caucvgsr  7574  pitonnlem1  7617  axi2m1  7647  axcnre  7653  axcaucvg  7672  mvrraddi  7943  mvlladdi  7944  negsubdi  7982  mul02  8113  mulneg1  8121  mulreim  8329  recextlem1  8372  recdivap  8438  2p2e4  8798  2times  8799  3p2e5  8812  3p3e6  8813  4p2e6  8814  4p3e7  8815  4p4e8  8816  5p2e7  8817  5p3e8  8818  5p4e9  8819  6p2e8  8820  6p3e9  8821  7p2e9  8822  1mhlfehlf  8889  8th4div3  8890  halfpm6th  8891  nneoor  9104  9p1e10  9135  dfdec10  9136  num0h  9144  numsuc  9146  dec10p  9175  numma  9176  nummac  9177  numma2c  9178  numadd  9179  numaddc  9180  nummul2c  9182  decaddci  9193  decsubi  9195  decmul1  9196  5p5e10  9203  6p4e10  9204  7p3e10  9207  8p2e10  9212  decbin0  9272  decbin2  9273  elfzp1b  9817  elfzm1b  9818  fz01or  9831  fz1ssfz0  9837  qbtwnrelemcalc  9973  fldiv4p1lem1div2  10018  1tonninf  10153  mulexpzap  10273  expaddzap  10277  sq4e2t8  10330  cu2  10331  i3  10334  iexpcyc  10337  binom2i  10341  binom3  10349  3dec  10401  faclbnd  10427  bcm1k  10446  bcp1nk  10448  bcpasc  10452  hashp1i  10496  hashxp  10512  imre  10563  crim  10570  remullem  10583  resqrexlemfp1  10721  resqrexlemover  10722  resqrexlemcalc1  10726  resqrexlemnm  10730  absexpzap  10792  absimle  10796  amgm2  10830  maxabslemlub  10919  fsumconst  11163  modfsummod  11167  binomlem  11192  binom11  11195  arisum  11207  arisum2  11208  georeclim  11222  geo2sum  11223  mertenslemi1  11244  mertenslem2  11245  mertensabs  11246  efzval  11288  resinval  11321  recosval  11322  efi4p  11323  tan0  11337  efival  11338  cosadd  11343  cos2tsin  11357  ef01bndlem  11362  cos1bnd  11365  cos2bnd  11366  absefib  11375  efieq1re  11376  demoivreALT  11378  eirraplem  11379  3dvdsdec  11458  3dvds2dec  11459  odd2np1  11466  nn0o1gt2  11498  nn0o  11500  flodddiv4  11527  algrp1  11623  3lcm2e6woprm  11663  nn0gcdsq  11773  phiprmpw  11793  cnmpt1res  12360  rerestcntop  12614  dvfvalap  12702  dvcnp2cntop  12715  dveflem  12738  ex-fl  12748  ex-exp  12750  ex-bc  12752  qdencn  13033  isomninnlem  13036
  Copyright terms: Public domain W3C validator