MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveqd Unicode version

Theorem oveqd 5962
Description: Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
Hypothesis
Ref Expression
oveq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
oveqd  |-  ( ph  ->  ( C A D )  =  ( C B D ) )

Proof of Theorem oveqd
StepHypRef Expression
1 oveq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 oveq 5951 . 2  |-  ( A  =  B  ->  ( C A D )  =  ( C B D ) )
31, 2syl 15 1  |-  ( ph  ->  ( C A D )  =  ( C B D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642  (class class class)co 5945
This theorem is referenced by:  oveq123d  5966  csbov12g  5977  ovmpt2dxf  6060  oprssov  6076  ofeq  6167  ruclem1  12606  vdwapval  13117  vdwapid1  13119  vdwmc2  13123  vdwpc  13124  vdwlem5  13129  vdwlem8  13132  vdwlem13  13137  prdsval  13454  prdsdsval2  13482  pwsplusgval  13488  pwsmulrval  13489  pwsvscafval  13492  imasval  13513  iscat  13673  iscatd  13674  catidex  13675  catideu  13676  cidfval  13677  cidval  13678  catidd  13681  iscatd2  13682  catlid  13684  catrid  13685  proplem3  13692  homffval  13693  homfeqd  13697  homfeqval  13699  comfffval  13700  comffval  13701  comfeq  13708  comfeqd  13709  comfeqval  13710  catpropd  13711  oppcval  13715  oppcco  13719  monfval  13734  ismon  13735  oppcmon  13740  oppcepi  13741  sectffval  13752  sectfval  13753  invffval  13759  isoval  13766  issubc  13811  issubc3  13822  fullresc  13824  isfunc  13837  cofuval  13855  cofuval2  13860  funcres  13869  funcres2b  13870  funcres2  13871  funcres2c  13874  isfull  13883  isfth  13887  fullres2c  13912  natfval  13919  isnat  13920  fucval  13931  fucco  13935  fucpropd  13950  homarcl  13959  coafval  13995  resssetc  14023  resscatc  14036  catciso  14038  xpcval  14050  1stfval  14064  2ndfval  14067  prfval  14072  prfcl  14076  evlfval  14090  curfval  14096  curf1  14098  curf1cl  14101  curfcl  14105  uncf1  14109  uncf2  14110  diag12  14117  diag2  14118  curf2ndf  14120  hofval  14125  hof1  14127  hof2fval  14128  hofcl  14132  yon12  14138  yon2  14139  hofpropd  14140  joinval  14221  meetval  14228  islat  14252  isdlat  14395  ismnd  14468  plusffval  14478  grpidval  14483  grpidd  14494  ismndd  14495  issubmnd  14500  submnd0  14501  ismhm  14516  issubm  14524  resmhm  14535  resmhm2  14536  resmhm2b  14537  gsumvalx  14550  gsumpropd  14552  gsumress  14553  isgrp  14592  isgrpd2e  14603  grpidd2  14618  grpinvfval  14619  imasgrp2  14709  imasgrp  14710  subg0  14726  subginv  14727  subgcl  14730  isnsg  14745  isghm  14782  resghm  14798  isga  14844  subgga  14853  gasubg  14855  cntzfval  14895  resscntz  14906  odfval  14947  gexval  14988  sylow2blem2  15031  lsmfval  15048  lsmvalx  15049  oppglsm  15052  subglsm  15081  pj1fval  15102  efgtval  15131  iscmn  15195  iscmnd  15200  submcmn2  15234  iscyg  15265  isrng  15444  rngidss  15466  isrngd  15474  prdsmgp  15492  mulgass3  15518  dvdsrval  15526  isirred  15580  isdrngd  15636  isdrngrd  15637  subrg1  15654  subrgmcl  15656  subrgdvds  15658  subrguss  15659  subrginv  15660  subrgdv  15661  subrgunit  15662  subrgugrp  15663  abvfval  15682  isabvd  15684  issrngd  15725  islmod  15730  islmodd  15732  scaffval  15744  lmodpropd  15787  lssset  15790  islssd  15792  prdslmodd  15825  islmhm  15883  reslmhm  15908  reslmhm2  15909  reslmhm2b  15910  islbs  15928  issubgrpd2  16040  rlmvneg  16058  rrgval  16127  isdomn  16134  isassa  16155  isassad  16162  psrval  16209  resspsradd  16259  resspsrmul  16260  resspsrvsca  16261  mplmon2mul  16341  ply1coe  16467  isphl  16638  ipffval  16658  isphld  16664  ocvfval  16672  isobs  16726  xkocnv  17611  submtmd  17889  prdsdsf  18033  ressprdsds  18037  blfval  18049  prdsxmslem2  18177  tmsxpsval  18186  ngpds  18227  subgngp  18253  tngngp  18272  isnlm  18288  lssnlm  18313  isphtpy  18583  isphtpc  18596  pi1cpbl  18646  pi1addf  18649  pi1addval  18650  pi1grplem  18651  clmsub  18682  clmvsass  18689  clmvsdir  18690  iscph  18710  cphdir  18744  cphdi  18745  cph2di  18746  cph2subdi  18749  cphass  18750  tchval  18754  ipcau2  18768  tchcphlem1  18769  tchcphlem2  18770  caufval  18805  dvlip2  19446  evl1expd  19525  q1pval  19643  r1pval  19646  dvntaylp  19854  dchrmul  20599  grpodivval  21022  gxval  21037  subgoov  21084  isrngo  21157  vcoprne  21249  dipfval  21389  ipval  21390  sspgval  21419  sspsval  21421  lnoval  21444  ajfval  21501  dipdir  21534  dipass  21537  htth  21612  rdivmuldivd  23419  zlm0  23621  zlm1  23622  istotbnd  25816  isbnd  25827  rrnequiv  25882  rngohomval  25918  idlval  25961  pridlval  25981  frlmplusgval  26552  frlmvscafval  26553  frlmup1  26573  lsslindf  26623  mamufval  26766  matplusg2  26800  matvsca2  26801  mat1  26805  mendval  26814  wlkon  27682  trlon  27692  trlonprop  27694  pthon  27717  pthonprop  27719  isconngra  27796  isconngra1  27797  lflset  29318  islfld  29321  ldualvadd  29388  ldualsmul  29394  ldualvs  29396  isopos  29439  cmtfvalN  29469  iscvlat  29582  ishlat1  29611  lineset  29996  psubspset  30002  paddfval  30055  paddval  30056  ltrnfset  30375  trnfsetN  30413  trlfset  30418  tgrpov  31006  erngplus  31061  erngmul  31064  erngplus-rN  31069  erngmul-rN  31072  erngdvlem3  31248  erngdvlem4  31249  erng0g  31252  erngdvlem3-rN  31256  erngdvlem4-rN  31257  dvaplusg  31267  dvamulr  31270  dvavadd  31273  dvavsca  31275  dvalveclem  31284  dvhmulr  31345  dvhfvadd  31350  dvhvadd  31351  dvhopvadd2  31353  dvhvaddcl  31354  dvhvaddcomN  31355  dvhvsca  31360  dvhlveclem  31367  dvh0g  31370  djavalN  31394  diblsmopel  31430  dicvaddcl  31449  cdlemn6  31461  dihffval  31489  dihopelvalcpre  31507  djhval  31657  lcdvaddval  31857  lcdsmul  31861  lcdvsval  31863  lcdlkreq2N  31882  hvmapffval  32017  hvmapfval  32018  hdmap1fval  32056  hgmapffval  32147  hgmapfval  32148  hgmapadd  32156  hlhilipval  32211  hlhilhillem  32222
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rex 2625  df-uni 3909  df-br 4105  df-iota 5301  df-fv 5345  df-ov 5948
  Copyright terms: Public domain W3C validator