ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  oveq2d 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-bndl 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  6415  addnq0mo  6430  mulnq0mo  6431  addnnnq0  6432  nq0a0  6440  distrnq0  6442  addassnq0  6445  prarloclemlo  6477  prarloclem3  6480  prarloclem5  6483  prarloclemcalc  6485  addnqprl  6512  addnqpru  6513  prmuloclemcalc  6546  mulnqprl  6549  mulnqpru  6550  distrlem4prl  6560  distrlem4pru  6561  1idprl  6566  1idpru  6567  ltexprlemloc  6581  addcanprleml  6588  addcanprlemu  6589  recexprlem1ssu  6606  ltmprr  6614  cauappcvgprlemcan  6616  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  cauappcvgprlemlim  6633  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemcl  6647  caucvgprlemladdrl  6649  caucvgprlem1  6650  caucvgpr  6653  addcmpblnr  6667  mulcmpblnrlemg  6668  addsrmo  6671  mulsrmo  6672  addsrpr  6673  mulsrpr  6674  ltsrprg  6675  recexgt0sr  6701  mulgt0sr  6704  mulcnsr  6732  axmulcom  6755  axmulass  6757  axdistr  6758  ax0id  6762  axcnre  6765  mulid1  6822  mul32  6940  mul31  6941  add32  6967  add4  6969  add42  6970  cnegex  6986  addcan2  6989  addsubass  7018  subsub2  7035  nppcan2  7038  sub32  7041  nnncan  7042  sub4  7052  muladd  7177  subdi  7178  mul2neg  7191  submul2  7192  mulsub  7194  mulsubfacd  7211  add20  7264  recexre  7362  rereim  7370  apreap  7371  ltmul1  7376  cru  7386  apreim  7387  mulreim  7388  apadd1  7392  apneg  7395  mulap0  7417  divrecap  7449  divassap  7451  divsubdirap  7466  divdivdivap  7471  divmul24ap  7474  divmuleqap  7475  divcanap6  7477  divdivap1  7481  divdivap2  7482  divsubdivap  7486  conjmulap  7487  div2negap  7493  apmul1  7546  cju  7694  nnmulcl  7716  add1p1  7951  sub1m1  7952  cnm2m1cnm3  7953  un0addcl  7991  un0mulcl  7992  zaddcllemneg  8060  qapne  8350  cnref1o  8357  lincmb01cmp  8641  iccf1o  8642  ige3m2fz  8683  fztp  8710  fzsuc2  8711  fseq1m1p1  8727  fzm1  8732  ige2m1fz1  8741  nn0split  8764  fzval3  8830  zpnn0elfzo1  8834  fzosplitsnm1  8835  fzosplitprm1  8860  fzoshftral  8864  iseqeq3  8896  iseqval  8900  iseqp1  8904  iseqfveq2  8905  expivallem  8910  expival  8911  expp1  8916  expnegap0  8917  expineg2  8918  expn1ap0  8919  expm1t  8937  1exp  8938  expnegzap  8943  mulexpzap  8949  expadd  8951  expaddzaplem  8952  expaddzap  8953  expmul  8954  expmulzap  8955  expsubap  8956  expp1zap  8957  expm1ap  8958  expdivap  8959  subsq2  9012  binom2  9015  binom21  9016  binom2sub  9017  binom3  9019  zesq  9020  bernneq  9022  cjval  9073  cjth  9074  crre  9085  replim  9087  remim  9088  reim0b  9090  rereb  9091  mulreap  9092  cjreb  9094  recj  9095  reneg  9096  readd  9097  resub  9098  remullem  9099  imcj  9103  imneg  9104  imadd  9105  imsub  9106  cjcj  9111  cjadd  9112  ipcnval  9114  cjmulrcl  9115  cjneg  9118  addcj  9119  cjsub  9120  cnrecnv  9138  absneg  9219  abscj  9220  absid  9225  absre  9228
  Copyright terms: Public domain W3C validator