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

Theorem oveq2i 5617
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 5614 . 2  |-  ( A  =  B  ->  ( C F A )  =  ( C F B ) )
31, 2ax-mp 7 1  |-  ( C F A )  =  ( C F B )
Colors of variables: wff set class
Syntax hints:    = wceq 1287  (class class class)co 5606
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 3436  df-pr 3437  df-op 3439  df-uni 3636  df-br 3820  df-iota 4942  df-fv 4985  df-ov 5609
This theorem is referenced by:  caov32  5782  oa1suc  6175  nnm1  6228  nnm2  6229  mapsnconst  6396  mapsncnv  6397  mulidnq  6884  halfnqq  6905  addpinq1  6959  addnqpr1  7057  caucvgprlemm  7163  caucvgprprlemval  7183  caucvgprprlemnbj  7188  caucvgprprlemmu  7190  caucvgprprlemaddq  7203  caucvgprprlem1  7204  caucvgprprlem2  7205  m1p1sr  7242  m1m1sr  7243  0idsr  7249  1idsr  7250  00sr  7251  pn0sr  7253  caucvgsrlemoffres  7281  caucvgsr  7283  mulresr  7311  pitonnlem2  7320  axi2m1  7346  ax1rid  7348  axcnre  7352  add42i  7584  negid  7665  negsub  7666  subneg  7667  negsubdii  7703  apreap  7997  recexaplem2  8052  muleqadd  8068  crap0  8345  2p2e4  8469  3p2e5  8483  3p3e6  8484  4p2e6  8485  4p3e7  8486  4p4e8  8487  5p2e7  8488  5p3e8  8489  5p4e9  8490  6p2e8  8491  6p3e9  8492  7p2e9  8493  3t3e9  8499  8th4div3  8560  halfpm6th  8561  iap0  8564  addltmul  8577  div4p1lem1div2  8594  peano2z  8711  nn0n0n1ge2  8742  nneoor  8773  zeo  8776  numsuc  8814  numltc  8826  numsucc  8840  numma  8844  nummul1c  8849  decrmac  8858  decsubi  8863  decmul1  8864  decmul10add  8869  6p5lem  8870  5p5e10  8871  6p4e10  8872  7p3e10  8875  8p2e10  8880  4t3lem  8897  9t11e99  8930  decbin2  8941  fztp  9414  fzprval  9418  fztpval  9419  fzshftral  9444  fz0tp  9455  fzo01  9547  fzo12sn  9548  fzo0to2pr  9549  fzo0to3tp  9550  fzo0to42pr  9551  intqfrac2  9646  intfracq  9647  sqval  9903  cu2  9942  i3  9945  i4  9946  binom2i  9952  binom3  9959  3dec  10011  faclbnd  10037  faclbnd2  10038  bcn1  10054  bcn2  10060  4bc3eq4  10069  4bc2eq6  10070  reim0  10182  cji  10223  resqrexlemover  10330  resqrexlemcalc1  10334  resqrexlemcalc3  10336  absi  10379  3dvdsdec  10731  3dvds2dec  10732  odd2np1lem  10738  odd2np1  10739  oddp1even  10742  mod2eq1n2dvds  10745  opoe  10761  6gcd4e2  10850  lcmneg  10922  3lcm2e6woprm  10934  6lcm4e12  10935  3prm  10976  3lcm2e6  11005  sqrt2irrlem  11006  pw2dvdslemn  11009  phiprm  11065  ex-bc  11085  ex-gcd  11087
  Copyright terms: Public domain W3C validator