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

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

Proof of Theorem oveq2i
StepHypRef Expression
1 oveq1i.1 . 2  |-  A  =  B
2 oveq2 5748 . 2  |-  ( A  =  B  ->  ( C F A )  =  ( C F B ) )
31, 2ax-mp 5 1  |-  ( C F A )  =  ( C F B )
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:  caov32  5924  oa1suc  6329  nnm1  6386  nnm2  6387  mapsnconst  6554  mapsncnv  6555  mulidnq  7161  halfnqq  7182  addpinq1  7236  addnqpr1  7334  caucvgprlemm  7440  caucvgprprlemval  7460  caucvgprprlemnbj  7465  caucvgprprlemmu  7467  caucvgprprlemaddq  7480  caucvgprprlem1  7481  caucvgprprlem2  7482  m1p1sr  7532  m1m1sr  7533  0idsr  7539  1idsr  7540  00sr  7541  pn0sr  7543  ltm1sr  7549  caucvgsrlemoffres  7572  caucvgsr  7574  mulresr  7610  pitonnlem2  7619  axi2m1  7647  ax1rid  7649  axcnre  7653  add42i  7892  negid  7973  negsub  7974  subneg  7975  negsubdii  8011  apreap  8312  recexaplem2  8376  muleqadd  8392  crap0  8676  2p2e4  8801  3p2e5  8815  3p3e6  8816  4p2e6  8817  4p3e7  8818  4p4e8  8819  5p2e7  8820  5p3e8  8821  5p4e9  8822  6p2e8  8823  6p3e9  8824  7p2e9  8825  3t3e9  8831  8th4div3  8893  halfpm6th  8894  iap0  8897  addltmul  8910  div4p1lem1div2  8927  peano2z  9044  nn0n0n1ge2  9075  nneoor  9107  zeo  9110  numsuc  9149  numltc  9161  numsucc  9175  numma  9179  nummul1c  9184  decrmac  9193  decsubi  9198  decmul1  9199  decmul10add  9204  6p5lem  9205  5p5e10  9206  6p4e10  9207  7p3e10  9210  8p2e10  9215  4t3lem  9232  9t11e99  9265  decbin2  9276  fztp  9809  fzprval  9813  fztpval  9814  fzshftral  9839  fz0tp  9852  fzo01  9944  fzo12sn  9945  fzo0to2pr  9946  fzo0to3tp  9947  fzo0to42pr  9948  intqfrac2  10043  intfracq  10044  sqval  10302  sq4e2t8  10341  cu2  10342  i3  10345  i4  10346  binom2i  10352  binom3  10360  3dec  10412  faclbnd  10438  faclbnd2  10439  bcn1  10455  bcn2  10461  4bc3eq4  10470  4bc2eq6  10471  reim0  10584  cji  10625  resqrexlemover  10733  resqrexlemcalc1  10737  resqrexlemcalc3  10739  absi  10782  fsump1i  11153  fsumconst  11174  modfsummodlemstep  11177  arisum2  11219  geoihalfsum  11242  mertenslemi1  11255  mertenslem2  11256  mertensabs  11257  ef0lem  11276  ege2le3  11287  eft0val  11309  ef4p  11310  efgt1p2  11311  efgt1p  11312  tanval2ap  11330  efival  11349  ef01bndlem  11373  sin01bnd  11374  cos01bnd  11375  cos1bnd  11376  cos2bnd  11377  3dvdsdec  11469  3dvds2dec  11470  odd2np1lem  11476  odd2np1  11477  oddp1even  11480  mod2eq1n2dvds  11483  opoe  11499  6gcd4e2  11590  lcmneg  11662  3lcm2e6woprm  11674  6lcm4e12  11675  3prm  11716  3lcm2e6  11745  sqrt2irrlem  11746  pw2dvdslemn  11749  phiprm  11805  restin  12251  uptx  12349  cnrehmeocntop  12668  dvexp  12750  dvmptidcn  12753  dvmptccn  12754  dveflem  12761  ex-exp  12773  ex-bc  12775  ex-gcd  12777  cvgcmp2nlemabs  13061
  Copyright terms: Public domain W3C validator