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

Theorem oveq2d 5515
Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
Hypothesis
Ref Expression
oveq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
oveq2d (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Proof of Theorem oveq2d
StepHypRef Expression
1 oveq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 oveq2 5507 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243  (class class class)co 5499
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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2309  df-v 2556  df-un 2919  df-sn 3378  df-pr 3379  df-op 3381  df-uni 3578  df-br 3762  df-iota 4854  df-fv 4897  df-ov 5502
This theorem is referenced by:  csbov1g  5532  caovassg  5646  caovdig  5662  caovdirg  5665  caov32d  5668  caov4d  5672  caov42d  5674  grprinvlem  5682  grprinvd  5683  grpridd  5684  nnaass  6051  nndi  6052  nnmass  6053  nnmsucr  6054  ecovass  6202  ecoviass  6203  ecovdi  6204  ecovidi  6205  addasspig  6409  mulasspig  6411  distrpig  6412  dfplpq2  6433  mulpipq2  6450  addassnqg  6461  prarloclemarch  6497  prarloclemarch2  6498  ltrnqg  6499  enq0sym  6511  addnq0mo  6526  mulnq0mo  6527  addnnnq0  6528  nq0a0  6536  distrnq0  6538  addassnq0  6541  prarloclemlo  6573  prarloclem3  6576  prarloclem5  6579  prarloclemcalc  6581  addnqprl  6608  addnqpru  6609  prmuloclemcalc  6644  mulnqprl  6647  mulnqpru  6648  distrlem4prl  6663  distrlem4pru  6664  1idprl  6669  1idpru  6670  ltexprlemloc  6686  addcanprleml  6693  addcanprlemu  6694  recexprlem1ssu  6713  ltmprr  6721  caucvgprlemcanl  6723  cauappcvgprlemladdru  6735  cauappcvgprlemladdrl  6736  cauappcvgprlem1  6738  cauappcvgprlemlim  6740  caucvgprlemnkj  6745  caucvgprlemnbj  6746  caucvgprlemdisj  6753  caucvgprlemloc  6754  caucvgprlemcl  6755  caucvgprlemladdrl  6757  caucvgprlem1  6758  caucvgpr  6761  caucvgprprlemell  6764  caucvgprprlemcbv  6766  caucvgprprlemval  6767  caucvgprprlemnkeqj  6769  caucvgprprlemopl  6776  caucvgprprlemlol  6777  caucvgprprlemloc  6782  caucvgprprlemclphr  6784  caucvgprprlemexb  6786  caucvgprprlemaddq  6787  caucvgprprlem1  6788  addcmpblnr  6805  mulcmpblnrlemg  6806  addsrmo  6809  mulsrmo  6810  addsrpr  6811  mulsrpr  6812  ltsrprg  6813  recexgt0sr  6839  mulgt0sr  6843  caucvgsrlemgt1  6860  caucvgsrlemoffval  6861  caucvgsr  6867  mulcnsr  6892  pitoregt0  6906  recidpirqlemcalc  6914  axmulcom  6926  axmulass  6928  axdistr  6929  ax0id  6933  axcnre  6936  recriota  6945  axcaucvglemcau  6953  axcaucvglemres  6954  mulid1  7005  mul32  7123  mul31  7124  add32  7150  add4  7152  add42  7153  cnegex  7169  addcan2  7172  addsubass  7201  subsub2  7218  nppcan2  7221  sub32  7224  nnncan  7225  sub4  7235  muladd  7360  subdi  7361  mul2neg  7374  submul2  7375  mulsub  7377  mulsubfacd  7394  add20  7447  recexre  7545  rereim  7553  apreap  7554  ltmul1  7559  cru  7569  apreim  7570  mulreim  7571  apadd1  7575  apneg  7578  mulap0  7611  divrecap  7643  divassap  7645  divsubdirap  7660  divdivdivap  7665  divmul24ap  7668  divmuleqap  7669  divcanap6  7671  divdivap1  7675  divdivap2  7676  divsubdivap  7680  conjmulap  7681  div2negap  7687  apmul1  7740  cju  7889  nnmulcl  7911  add1p1  8147  sub1m1  8148  cnm2m1cnm3  8149  un0addcl  8187  un0mulcl  8188  zaddcllemneg  8256  qapne  8546  cnref1o  8553  lincmb01cmp  8838  iccf1o  8839  ige3m2fz  8880  fztp  8907  fzsuc2  8908  fseq1m1p1  8924  fzm1  8929  ige2m1fz1  8938  nn0split  8961  fzval3  9027  zpnn0elfzo1  9031  fzosplitsnm1  9032  fzosplitprm1  9057  fzoshftral  9061  iseqeq3  9094  iseqval  9098  iseqp1  9103  iseqm1  9105  iseqfveq2  9106  iseqshft2  9110  monoord2  9114  isermono  9115  iseqsplit  9116  iseqcaopr3  9118  iseqcaopr2  9119  iseqcaopr  9120  iseqhomo  9126  expivallem  9134  expival  9135  expp1  9140  expnegap0  9141  expineg2  9142  expn1ap0  9143  expm1t  9161  1exp  9162  expnegzap  9167  mulexpzap  9173  expadd  9175  expaddzaplem  9176  expaddzap  9177  expmul  9178  expmulzap  9179  expsubap  9180  expp1zap  9181  expm1ap  9182  expdivap  9183  subsq2  9237  binom2  9240  binom21  9241  binom2sub  9242  binom3  9244  zesq  9245  bernneq  9247  shftcan1  9313  shftcan2  9314  cjval  9323  cjth  9324  crre  9335  replim  9337  remim  9338  reim0b  9340  rereb  9341  mulreap  9342  cjreb  9344  recj  9345  reneg  9346  readd  9347  resub  9348  remullem  9349  imcj  9353  imneg  9354  imadd  9355  imsub  9356  cjcj  9361  cjadd  9362  ipcnval  9364  cjmulrcl  9365  cjneg  9368  addcj  9369  cjsub  9370  cnrecnv  9388  caucvgrelemcau  9457  cvg1nlemcau  9461  cvg1nlemres  9462  recvguniqlem  9470  resqrexlemover  9486  resqrexlemlo  9489  resqrexlemcalc1  9490  resqrexlemcalc3  9492  resqrexlemnm  9494  resqrexlemcvg  9495  absneg  9526  abscj  9528  sqabsadd  9531  sqabssub  9532  absmul  9545  absid  9547  absre  9551  absresq  9552  absexpzap  9554  recvalap  9571  abstri  9578  abs2dif2  9581  recan  9583  cau3lem  9588  amgm2  9592  climaddc1  9726  climsubc1  9729  climcvg1nlem  9745  serif0  9748
  Copyright terms: Public domain W3C validator