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

Theorem oveq2d 5440
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 5432 . 2 (A = B → (𝐶𝐹A) = (𝐶𝐹B))
31, 2syl 14 1 (φ → (𝐶𝐹A) = (𝐶𝐹B))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1223  (class class class)co 5424
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 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995
This theorem depends on definitions:  df-bi 110  df-3an 869  df-tru 1226  df-nf 1323  df-sb 1619  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-rex 2281  df-v 2528  df-un 2890  df-sn 3345  df-pr 3346  df-op 3348  df-uni 3544  df-br 3728  df-iota 4782  df-fv 4825  df-ov 5427
This theorem is referenced by:  csbov1g  5456  caovassg  5570  caovdig  5586  caovdirg  5589  caov32d  5592  caov4d  5596  caov42d  5598  grprinvlem  5606  grprinvd  5607  grpridd  5608  nnaass  5967  nndi  5968  nnmass  5969  nnmsucr  5970  ecovass  6114  ecoviass  6115  ecovdi  6116  ecovidi  6117  addasspig  6176  mulasspig  6178  distrpig  6179  dfplpq2  6199  mulpipq2  6216  addassnqg  6227  prarloclemarch  6261  prarloclemarch2  6262  ltrnqg  6263  enq0sym  6273  addnq0mo  6288  mulnq0mo  6289  addnnnq0  6290  nq0a0  6298  distrnq0  6300  addassnq0  6303  prarloclemlo  6334  prarloclem3  6337  prarloclem5  6340  prarloclemcalc  6342  addnqprl  6370  addnqpru  6371  prmuloclemcalc  6395  mulnqprl  6398  mulnqpru  6399  distrlem4prl  6409  distrlem4pru  6410  1idprl  6415  1idpru  6416  ltexprlemloc  6430  addcanprleml  6437  addcanprlemu  6438  recexprlem1ssu  6455  ltmprr  6463  addcmpblnr  6477  mulcmpblnrlemg  6478  addsrmo  6481  mulsrmo  6482  addsrpr  6483  mulsrpr  6484  ltsrprg  6485  recexgt0sr  6511  mulgt0sr  6514  mulcnsr  6541  axmulcom  6560  axmulass  6562  axdistr  6563  ax0id  6567  axcnre  6570  mulid1  6625  mul32  6743  mul31  6744  add32  6770  add4  6772  add42  6773  cnegex  6789  addcan2  6792  addsubass  6821  subsub2  6838  nppcan2  6841  sub32  6844  nnncan  6845  sub4  6855  muladd  6980  subdi  6981  mul2neg  6994  submul2  6995  mulsub  6997  mulsubfacd  7014  add20  7067  recexre  7165  rereim  7173  apreap  7174  ltmul1  7179  cru  7189  apreim  7190  mulreim  7191  apadd1  7195  apneg  7198  mulap0  7220  divrecap  7252  divassap  7254  divsubdirap  7269  divdivdivap  7274  divmul24ap  7277  divmuleqap  7278  divcanap6  7280  divdivap1  7284  divdivap2  7285  divsubdivap  7289  conjmulap  7290  div2negap  7296  apmul1  7349  cju  7496  nnmulcl  7518  add1p1  7752  sub1m1  7753  cnm2m1cnm3  7754  un0addcl  7789  un0mulcl  7790  zaddcllemneg  7857  qapne  8056
  Copyright terms: Public domain W3C validator