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

Theorem oveq2i 5792
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)
Hypothesis
Ref Expression
oveq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
oveq2i (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Proof of Theorem oveq2i
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq2 5789 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2ax-mp 5 1 (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Colors of variables: wff set class
Syntax hints:   = wceq 1332  (class class class)co 5781
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3079  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-iota 5095  df-fv 5138  df-ov 5784
This theorem is referenced by:  caov32  5965  oa1suc  6370  nnm1  6427  nnm2  6428  mapsnconst  6595  mapsncnv  6596  mulidnq  7220  halfnqq  7241  addpinq1  7295  addnqpr1  7393  caucvgprlemm  7499  caucvgprprlemval  7519  caucvgprprlemnbj  7524  caucvgprprlemmu  7526  caucvgprprlemaddq  7539  caucvgprprlem1  7540  caucvgprprlem2  7541  m1p1sr  7591  m1m1sr  7592  0idsr  7598  1idsr  7599  00sr  7600  pn0sr  7602  ltm1sr  7608  caucvgsrlemoffres  7631  caucvgsr  7633  mulresr  7669  pitonnlem2  7678  axi2m1  7706  ax1rid  7708  axcnre  7712  add42i  7951  negid  8032  negsub  8033  subneg  8034  negsubdii  8070  apreap  8372  recexaplem2  8436  muleqadd  8452  crap0  8739  2p2e4  8870  3p2e5  8884  3p3e6  8885  4p2e6  8886  4p3e7  8887  4p4e8  8888  5p2e7  8889  5p3e8  8890  5p4e9  8891  6p2e8  8892  6p3e9  8893  7p2e9  8894  3t3e9  8900  8th4div3  8962  halfpm6th  8963  iap0  8966  addltmul  8979  div4p1lem1div2  8996  peano2z  9113  nn0n0n1ge2  9144  nneoor  9176  zeo  9179  numsuc  9218  numltc  9230  numsucc  9244  numma  9248  nummul1c  9253  decrmac  9262  decsubi  9267  decmul1  9268  decmul10add  9273  6p5lem  9274  5p5e10  9275  6p4e10  9276  7p3e10  9279  8p2e10  9284  4t3lem  9301  9t11e99  9334  decbin2  9345  fztp  9888  fzprval  9892  fztpval  9893  fzshftral  9918  fz0tp  9931  fzo01  10023  fzo12sn  10024  fzo0to2pr  10025  fzo0to3tp  10026  fzo0to42pr  10027  intqfrac2  10122  intfracq  10123  sqval  10381  sq4e2t8  10420  cu2  10421  i3  10424  i4  10425  binom2i  10431  binom3  10439  3dec  10491  faclbnd  10518  faclbnd2  10519  bcn1  10535  bcn2  10541  4bc3eq4  10550  4bc2eq6  10551  reim0  10664  cji  10705  resqrexlemover  10813  resqrexlemcalc1  10817  resqrexlemcalc3  10819  absi  10862  fsump1i  11233  fsumconst  11254  modfsummodlemstep  11257  arisum2  11299  geoihalfsum  11322  mertenslemi1  11335  mertenslem2  11336  mertensabs  11337  ef0lem  11401  ege2le3  11412  eft0val  11434  ef4p  11435  efgt1p2  11436  efgt1p  11437  tanval2ap  11454  efival  11473  ef01bndlem  11497  sin01bnd  11498  cos01bnd  11499  cos1bnd  11500  cos2bnd  11501  3dvdsdec  11596  3dvds2dec  11597  odd2np1lem  11603  odd2np1  11604  oddp1even  11607  mod2eq1n2dvds  11610  opoe  11626  6gcd4e2  11717  lcmneg  11789  3lcm2e6woprm  11801  6lcm4e12  11802  3prm  11843  3lcm2e6  11872  sqrt2irrlem  11873  pw2dvdslemn  11877  phiprm  11933  restin  12382  uptx  12480  cnrehmeocntop  12799  dvexp  12881  dvmptidcn  12884  dvmptccn  12885  dveflem  12893  sinhalfpilem  12918  efhalfpi  12926  cospi  12927  efipi  12928  sin2pi  12930  cos2pi  12931  ef2pi  12932  sin2pim  12940  cos2pim  12941  sinmpi  12942  cosmpi  12943  sinppi  12944  cosppi  12945  sincosq4sgn  12956  tangtx  12965  sincos4thpi  12967  sincos6thpi  12969  sincos3rdpi  12970  abssinper  12973  cosq34lt1  12977  1cxp  13027  ecxp  13028  rpcxpsqrt  13048  rpelogb  13072  2logb9irrALT  13097  ex-exp  13108  ex-bc  13110  ex-gcd  13112  cvgcmp2nlemabs  13400
  Copyright terms: Public domain W3C validator