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  6512  addnqpru  6513  prmuloclemcalc  6544  mulnqprl  6547  mulnqpru  6548  distrlem4prl  6558  distrlem4pru  6559  1idprl  6564  1idpru  6565  ltexprlemloc  6579  addcanprleml  6586  addcanprlemu  6587  recexprlem1ssu  6604  ltmprr  6612  addcmpblnr  6627  mulcmpblnrlemg  6628  addsrmo  6631  mulsrmo  6632  addsrpr  6633  mulsrpr  6634  ltsrprg  6635  recexgt0sr  6661  mulgt0sr  6664  mulcnsr  6692  axmulcom  6715  axmulass  6717  axdistr  6718  ax0id  6722  axcnre  6725  mulid1  6782  mul32  6900  mul31  6901  add32  6927  add4  6929  add42  6930  cnegex  6946  addcan2  6949  addsubass  6978  subsub2  6995  nppcan2  6998  sub32  7001  nnncan  7002  sub4  7012  muladd  7137  subdi  7138  mul2neg  7151  submul2  7152  mulsub  7154  mulsubfacd  7171  add20  7224  recexre  7322  rereim  7330  apreap  7331  ltmul1  7336  cru  7346  apreim  7347  mulreim  7348  apadd1  7352  apneg  7355  mulap0  7377  divrecap  7409  divassap  7411  divsubdirap  7426  divdivdivap  7431  divmul24ap  7434  divmuleqap  7435  divcanap6  7437  divdivap1  7441  divdivap2  7442  divsubdivap  7446  conjmulap  7447  div2negap  7453  apmul1  7506  cju  7654  nnmulcl  7676  add1p1  7911  sub1m1  7912  cnm2m1cnm3  7913  un0addcl  7951  un0mulcl  7952  zaddcllemneg  8020  qapne  8310  cnref1o  8317  lincmb01cmp  8601  iccf1o  8602  ige3m2fz  8643  fztp  8670  fzsuc2  8671  fseq1m1p1  8687  fzm1  8692  ige2m1fz1  8701  nn0split  8724  fzval3  8790  zpnn0elfzo1  8794  fzosplitsnm1  8795  fzosplitprm1  8820  fzoshftral  8824  iseqeq3  8856  iseqval  8860  iseqp1  8864  iseqfveq2  8865  expivallem  8870  expival  8871  expp1  8876  expnegap0  8877  expineg2  8878  expn1ap0  8879  expm1t  8897  1exp  8898  expnegzap  8903  mulexpzap  8909  expadd  8911  expaddzaplem  8912  expaddzap  8913  expmul  8914  expmulzap  8915  expsubap  8916  expp1zap  8917  expm1ap  8918  expdivap  8919  subsq2  8972  binom2  8975  binom21  8976  binom2sub  8977  binom3  8979  zesq  8980  bernneq  8982  cjval  9033  cjth  9034  crre  9045  replim  9047  remim  9048  reim0b  9050  rereb  9051  mulreap  9052  cjreb  9054  recj  9055  reneg  9056  readd  9057  resub  9058  remullem  9059  imcj  9063  imneg  9064  imadd  9065  imsub  9066  cjcj  9071  cjadd  9072  ipcnval  9074  cjmulrcl  9075  cjneg  9078  addcj  9079  cjsub  9080  cnrecnv  9098
  Copyright terms: Public domain W3C validator