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

Theorem oveq1i 5750
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 5747 . 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 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  8375  recdivap  8441  2p2e4  8801  2times  8802  3p2e5  8815  3p3e6  8816  4p2e6  8817  4p3e7  8818  4p4e8  8819  5p2e7  8820  5p3e8  8821  5p4e9  8822  6p2e8  8823  6p3e9  8824  7p2e9  8825  1mhlfehlf  8892  8th4div3  8893  halfpm6th  8894  nneoor  9107  9p1e10  9138  dfdec10  9139  num0h  9147  numsuc  9149  dec10p  9178  numma  9179  nummac  9180  numma2c  9181  numadd  9182  numaddc  9183  nummul2c  9185  decaddci  9196  decsubi  9198  decmul1  9199  5p5e10  9206  6p4e10  9207  7p3e10  9210  8p2e10  9215  decbin0  9275  decbin2  9276  elfzp1b  9828  elfzm1b  9829  fz01or  9842  fz1ssfz0  9848  qbtwnrelemcalc  9984  fldiv4p1lem1div2  10029  1tonninf  10164  mulexpzap  10284  expaddzap  10288  sq4e2t8  10341  cu2  10342  i3  10345  iexpcyc  10348  binom2i  10352  binom3  10360  3dec  10412  faclbnd  10438  bcm1k  10457  bcp1nk  10459  bcpasc  10463  hashp1i  10507  hashxp  10523  imre  10574  crim  10581  remullem  10594  resqrexlemfp1  10732  resqrexlemover  10733  resqrexlemcalc1  10737  resqrexlemnm  10741  absexpzap  10803  absimle  10807  amgm2  10841  maxabslemlub  10930  fsumconst  11174  modfsummod  11178  binomlem  11203  binom11  11206  arisum  11218  arisum2  11219  georeclim  11233  geo2sum  11234  mertenslemi1  11255  mertenslem2  11256  mertensabs  11257  efzval  11299  resinval  11332  recosval  11333  efi4p  11334  tan0  11348  efival  11349  cosadd  11354  cos2tsin  11368  ef01bndlem  11373  cos1bnd  11376  cos2bnd  11377  absefib  11386  efieq1re  11387  demoivreALT  11389  eirraplem  11390  3dvdsdec  11469  3dvds2dec  11470  odd2np1  11477  nn0o1gt2  11509  nn0o  11511  flodddiv4  11538  algrp1  11634  3lcm2e6woprm  11674  nn0gcdsq  11784  phiprmpw  11804  cnmpt1res  12371  rerestcntop  12625  dvfvalap  12725  dvcnp2cntop  12738  dveflem  12761  ex-fl  12771  ex-exp  12773  ex-bc  12775  qdencn  13056  isomninnlem  13059
  Copyright terms: Public domain W3C validator