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

Theorem oveq1i 5623
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 5620 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2ax-mp 7 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐶)
Colors of variables: wff set class
Syntax hints:   = wceq 1287  (class class class)co 5613
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-br 3821  df-iota 4946  df-fv 4989  df-ov 5616
This theorem is referenced by:  caov12  5790  map1  6481  halfnqq  6913  prarloclem5  7003  m1m1sr  7251  caucvgsrlemfv  7280  caucvgsr  7291  pitonnlem1  7326  axi2m1  7354  axcnre  7360  axcaucvg  7379  mvrraddi  7643  mvlladdi  7644  negsubdi  7682  mul02  7809  mulneg1  7817  mulreim  8022  recextlem1  8059  recdivap  8124  2p2e4  8477  2times  8478  3p2e5  8491  3p3e6  8492  4p2e6  8493  4p3e7  8494  4p4e8  8495  5p2e7  8496  5p3e8  8497  5p4e9  8498  6p2e8  8499  6p3e9  8500  7p2e9  8501  1mhlfehlf  8567  8th4div3  8568  halfpm6th  8569  nneoor  8781  9p1e10  8811  dfdec10  8812  num0h  8820  numsuc  8822  dec10p  8851  numma  8852  nummac  8853  numma2c  8854  numadd  8855  numaddc  8856  nummul2c  8858  decaddci  8869  decsubi  8871  decmul1  8872  5p5e10  8879  6p4e10  8880  7p3e10  8883  8p2e10  8888  decbin0  8948  decbin2  8949  elfzp1b  9441  elfzm1b  9442  fz01or  9455  qbtwnrelemcalc  9595  fldiv4p1lem1div2  9640  1tonninf  9774  mulexpzap  9893  expaddzap  9897  cu2  9950  i3  9953  iexpcyc  9956  binom2i  9960  binom3  9967  3dec  10019  faclbnd  10045  bcm1k  10064  bcp1nk  10066  bcpasc  10070  hashp1i  10114  hashxp  10130  imre  10180  crim  10187  remullem  10200  resqrexlemfp1  10337  resqrexlemover  10338  resqrexlemcalc1  10342  resqrexlemnm  10346  absexpzap  10408  absimle  10412  amgm2  10446  maxabslemlub  10535  3dvdsdec  10740  3dvds2dec  10741  odd2np1  10748  nn0o1gt2  10780  nn0o  10782  flodddiv4  10809  3lcm2e6woprm  10943  nn0gcdsq  11053  phiprmpw  11073  ex-fl  11091  ex-bc  11094  qdencn  11353
  Copyright terms: Public domain W3C validator