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

Theorem oveq2d 5471
Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
Hypothesis
Ref Expression
oveq1d.1 (φA = B)
Assertion
Ref Expression
oveq2d (φ → (𝐶𝐹A) = (𝐶𝐹B))

Proof of Theorem oveq2d
StepHypRef Expression
1 oveq1d.1 . 2 (φA = B)
2 oveq2 5463 . 2 (A = B → (𝐶𝐹A) = (𝐶𝐹B))
31, 2syl 14 1 (φ → (𝐶𝐹A) = (𝐶𝐹B))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242  (class class class)co 5455
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458
This theorem is referenced by:  csbov1g  5487  caovassg  5601  caovdig  5617  caovdirg  5620  caov32d  5623  caov4d  5627  caov42d  5629  grprinvlem  5637  grprinvd  5638  grpridd  5639  nnaass  6003  nndi  6004  nnmass  6005  nnmsucr  6006  ecovass  6151  ecoviass  6152  ecovdi  6153  ecovidi  6154  addasspig  6314  mulasspig  6316  distrpig  6317  dfplpq2  6338  mulpipq2  6355  addassnqg  6366  prarloclemarch  6401  prarloclemarch2  6402  ltrnqg  6403  enq0sym  6414  addnq0mo  6429  mulnq0mo  6430  addnnnq0  6431  nq0a0  6439  distrnq0  6441  addassnq0  6444  prarloclemlo  6476  prarloclem3  6479  prarloclem5  6482  prarloclemcalc  6484  addnqprl  6511  addnqpru  6512  prmuloclemcalc  6545  mulnqprl  6548  mulnqpru  6549  distrlem4prl  6559  distrlem4pru  6560  1idprl  6565  1idpru  6566  ltexprlemloc  6580  addcanprleml  6587  addcanprlemu  6588  recexprlem1ssu  6605  ltmprr  6613  cauappcvgprlemcan  6615  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem1  6630  cauappcvgprlemlim  6632  addcmpblnr  6647  mulcmpblnrlemg  6648  addsrmo  6651  mulsrmo  6652  addsrpr  6653  mulsrpr  6654  ltsrprg  6655  recexgt0sr  6681  mulgt0sr  6684  mulcnsr  6712  axmulcom  6735  axmulass  6737  axdistr  6738  ax0id  6742  axcnre  6745  mulid1  6802  mul32  6920  mul31  6921  add32  6947  add4  6949  add42  6950  cnegex  6966  addcan2  6969  addsubass  6998  subsub2  7015  nppcan2  7018  sub32  7021  nnncan  7022  sub4  7032  muladd  7157  subdi  7158  mul2neg  7171  submul2  7172  mulsub  7174  mulsubfacd  7191  add20  7244  recexre  7342  rereim  7350  apreap  7351  ltmul1  7356  cru  7366  apreim  7367  mulreim  7368  apadd1  7372  apneg  7375  mulap0  7397  divrecap  7429  divassap  7431  divsubdirap  7446  divdivdivap  7451  divmul24ap  7454  divmuleqap  7455  divcanap6  7457  divdivap1  7461  divdivap2  7462  divsubdivap  7466  conjmulap  7467  div2negap  7473  apmul1  7526  cju  7674  nnmulcl  7696  add1p1  7931  sub1m1  7932  cnm2m1cnm3  7933  un0addcl  7971  un0mulcl  7972  zaddcllemneg  8040  qapne  8330  cnref1o  8337  lincmb01cmp  8621  iccf1o  8622  ige3m2fz  8663  fztp  8690  fzsuc2  8691  fseq1m1p1  8707  fzm1  8712  ige2m1fz1  8721  nn0split  8744  fzval3  8810  zpnn0elfzo1  8814  fzosplitsnm1  8815  fzosplitprm1  8840  fzoshftral  8844  iseqeq3  8876  iseqval  8880  iseqp1  8884  iseqfveq2  8885  expivallem  8890  expival  8891  expp1  8896  expnegap0  8897  expineg2  8898  expn1ap0  8899  expm1t  8917  1exp  8918  expnegzap  8923  mulexpzap  8929  expadd  8931  expaddzaplem  8932  expaddzap  8933  expmul  8934  expmulzap  8935  expsubap  8936  expp1zap  8937  expm1ap  8938  expdivap  8939  subsq2  8992  binom2  8995  binom21  8996  binom2sub  8997  binom3  8999  zesq  9000  bernneq  9002  cjval  9053  cjth  9054  crre  9065  replim  9067  remim  9068  reim0b  9070  rereb  9071  mulreap  9072  cjreb  9074  recj  9075  reneg  9076  readd  9077  resub  9078  remullem  9079  imcj  9083  imneg  9084  imadd  9085  imsub  9086  cjcj  9091  cjadd  9092  ipcnval  9094  cjmulrcl  9095  cjneg  9098  addcj  9099  cjsub  9100  cnrecnv  9118  absneg  9199  abscj  9200  absid  9205  absre  9208
  Copyright terms: Public domain W3C validator