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

Theorem oveq2i 5554
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 5551 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2ax-mp 7 1 (𝐶𝐹𝐴) = (𝐶𝐹𝐵)
Colors of variables: wff set class
Syntax hints:   = wceq 1285  (class class class)co 5543
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-iota 4897  df-fv 4940  df-ov 5546
This theorem is referenced by:  caov32  5719  oa1suc  6111  nnm1  6163  nnm2  6164  mulidnq  6641  halfnqq  6662  addpinq1  6716  addnqpr1  6814  caucvgprlemm  6920  caucvgprprlemval  6940  caucvgprprlemnbj  6945  caucvgprprlemmu  6947  caucvgprprlemaddq  6960  caucvgprprlem1  6961  caucvgprprlem2  6962  m1p1sr  6999  m1m1sr  7000  0idsr  7006  1idsr  7007  00sr  7008  pn0sr  7010  caucvgsrlemoffres  7038  caucvgsr  7040  mulresr  7068  pitonnlem2  7077  axi2m1  7103  ax1rid  7105  axcnre  7109  add42i  7341  negid  7422  negsub  7423  subneg  7424  negsubdii  7460  apreap  7754  recexaplem2  7809  muleqadd  7825  crap0  8102  2p2e4  8226  3p2e5  8240  3p3e6  8241  4p2e6  8242  4p3e7  8243  4p4e8  8244  5p2e7  8245  5p3e8  8246  5p4e9  8247  6p2e8  8248  6p3e9  8249  7p2e9  8250  3t3e9  8256  8th4div3  8317  halfpm6th  8318  iap0  8321  addltmul  8334  div4p1lem1div2  8351  peano2z  8468  nn0n0n1ge2  8499  nneoor  8530  zeo  8533  numsuc  8571  numltc  8583  numsucc  8597  numma  8601  nummul1c  8606  decrmac  8615  decsubi  8620  decmul1  8621  decmul10add  8626  6p5lem  8627  5p5e10  8628  6p4e10  8629  7p3e10  8632  8p2e10  8637  4t3lem  8654  9t11e99  8687  decbin2  8698  fztp  9171  fzprval  9175  fztpval  9176  fzshftral  9201  fz0tp  9212  fzo01  9302  fzo12sn  9303  fzo0to2pr  9304  fzo0to3tp  9305  fzo0to42pr  9306  intqfrac2  9401  intfracq  9402  sqval  9631  cu2  9670  i3  9673  i4  9674  binom2i  9680  binom3  9687  3dec  9739  faclbnd  9765  faclbnd2  9766  bcn1  9782  bcn2  9788  4bc3eq4  9797  4bc2eq6  9798  reim0  9886  cji  9927  resqrexlemover  10034  resqrexlemcalc1  10038  resqrexlemcalc3  10040  absi  10083  3dvdsdec  10409  3dvds2dec  10410  odd2np1lem  10416  odd2np1  10417  oddp1even  10420  mod2eq1n2dvds  10423  opoe  10439  6gcd4e2  10528  lcmneg  10600  3lcm2e6woprm  10612  6lcm4e12  10613  3prm  10654  3lcm2e6  10683  sqrt2irrlem  10684  pw2dvdslemn  10687  ex-bc  10717  ex-gcd  10719
  Copyright terms: Public domain W3C validator