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

Theorem oveqd 6061
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 6050 . 2  |-  ( A  =  B  ->  ( C A D )  =  ( C B D ) )
31, 2syl 16 1  |-  ( ph  ->  ( C A D )  =  ( C B D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649  (class class class)co 6044
This theorem is referenced by:  oveq123d  6065  csbov12g  6076  ovmpt2dxf  6162  oprssov  6178  ofeq  6270  ruclem1  12789  vdwapval  13300  vdwapid1  13302  vdwmc2  13306  vdwpc  13307  vdwlem5  13312  vdwlem8  13315  vdwlem13  13320  prdsval  13637  prdsdsval2  13665  pwsplusgval  13671  pwsmulrval  13672  pwsvscafval  13675  imasval  13696  iscat  13856  iscatd  13857  catidex  13858  catideu  13859  cidfval  13860  cidval  13861  catidd  13864  iscatd2  13865  catlid  13867  catrid  13868  proplem3  13875  homffval  13876  homfeqd  13880  homfeqval  13882  comfffval  13883  comffval  13884  comfeq  13891  comfeqd  13892  comfeqval  13893  catpropd  13894  oppcval  13898  oppcco  13902  monfval  13917  ismon  13918  oppcmon  13923  oppcepi  13924  sectffval  13935  sectfval  13936  invffval  13942  isoval  13949  issubc  13994  issubc3  14005  isfunc  14020  cofuval  14038  cofuval2  14043  funcres  14052  funcres2b  14053  funcres2  14054  funcres2c  14057  isfull  14066  isfth  14070  fullres2c  14095  natfval  14102  isnat  14103  fucval  14114  fucco  14118  fucpropd  14133  homarcl  14142  coafval  14178  resssetc  14206  resscatc  14219  catciso  14221  xpcval  14233  1stfval  14247  2ndfval  14250  prfval  14255  prfcl  14259  evlfval  14273  curfval  14279  curf1cl  14284  curfcl  14288  uncf1  14292  uncf2  14293  diag12  14300  diag2  14301  curf2ndf  14303  hofval  14308  hof1  14310  hof2fval  14311  hofcl  14315  yon12  14321  yon2  14322  hofpropd  14323  joinval  14404  meetval  14411  islat  14435  isdlat  14578  ismnd  14651  plusffval  14661  grpidval  14666  grpidd  14677  ismndd  14678  issubmnd  14683  submnd0  14684  ismhm  14699  issubm  14707  resmhm  14718  resmhm2  14719  resmhm2b  14720  gsumvalx  14733  gsumpropd  14735  gsumress  14736  isgrp  14775  isgrpd2e  14786  grpidd2  14801  grpinvfval  14802  imasgrp2  14892  imasgrp  14893  subg0  14909  subginv  14910  subgcl  14913  isnsg  14928  isghm  14965  resghm  14981  isga  15027  subgga  15036  gasubg  15038  cntzfval  15078  resscntz  15089  odfval  15130  gexval  15171  lsmfval  15231  lsmvalx  15232  oppglsm  15235  subglsm  15264  pj1fval  15285  efgtval  15314  iscmn  15378  iscmnd  15383  submcmn2  15417  iscyg  15448  isrng  15627  rngidss  15649  prdsmgp  15675  mulgass3  15701  dvdsrval  15709  isirred  15763  isdrngd  15819  isdrngrd  15820  subrg1  15837  subrgmcl  15839  subrgdvds  15841  subrguss  15842  subrginv  15843  subrgdv  15844  subrgunit  15845  subrgugrp  15846  abvfval  15865  isabvd  15867  issrngd  15908  islmod  15913  islmodd  15915  scaffval  15927  lmodpropd  15966  lssset  15969  islssd  15971  prdslmodd  16004  islmhm  16062  reslmhm  16087  reslmhm2  16088  reslmhm2b  16089  islbs  16107  issubgrpd2  16219  rlmvneg  16237  rrgval  16306  isassa  16334  isassad  16341  psrval  16388  resspsradd  16438  resspsrmul  16439  resspsrvsca  16440  mplmon2mul  16520  ply1coe  16643  isphl  16818  ipffval  16838  isphld  16844  ocvfval  16852  isobs  16906  xkocnv  17803  submtmd  18091  prdsdsf  18354  ressprdsds  18358  blfvalps  18370  prdsxmslem2  18516  tmsxpsval  18525  ngpds  18607  subgngp  18633  tngngp  18652  isnlm  18668  lssnlm  18693  isphtpy  18963  isphtpc  18976  pi1cpbl  19026  pi1addf  19029  pi1addval  19030  pi1grplem  19031  clmsub  19062  clmvsass  19069  clmvsdir  19070  iscph  19090  cphdir  19124  cphdi  19125  cph2di  19126  cph2subdi  19129  cphass  19130  tchval  19134  ipcau2  19148  tchcphlem1  19149  tchcphlem2  19150  caufval  19185  dvlip2  19836  evl1expd  19915  q1pval  20033  r1pval  20036  dvntaylp  20244  dchrmul  20989  wlkon  21487  trlon  21497  trlonprop  21499  pthon  21532  pthonprop  21534  spthon  21539  spthonprp  21542  isconngra  21616  isconngra1  21617  grpodivval  21788  gxval  21803  subgoov  21850  isrngo  21923  vcoprne  22015  dipfval  22155  ipval  22156  sspgval  22185  sspsval  22187  lnoval  22210  ajfval  22267  dipdir  22300  dipass  22303  htth  22378  rdivmuldivd  24184  isofld  24192  subofld  24202  inftmrel  24207  isinftm  24208  metidval  24242  pstmval  24247  pstmfval  24248  zlm0  24303  zlm1  24304  sitmval  24618  istotbnd  26372  isbnd  26383  rrnequiv  26438  rngohomval  26474  idlval  26517  pridlval  26537  frlmplusgval  27101  frlmvscafval  27102  frlmup1  27122  lsslindf  27172  mamufval  27315  matplusg2  27349  matvsca2  27350  mat1  27354  is2wlkonot  28064  is2spthonot  28065  2wlkonot  28066  2spthonot  28067  2wlksot  28068  2spthsot  28069  2wlkonot3v  28076  2spthonot3v  28077  lflset  29546  islfld  29549  ldualvadd  29616  ldualsmul  29622  ldualvs  29624  isopos  29667  cmtfvalN  29697  iscvlat  29810  ishlat1  29839  lineset  30224  psubspset  30230  paddfval  30283  paddval  30284  ltrnfset  30603  trnfsetN  30641  trlfset  30646  tgrpov  31234  erngplus  31289  erngmul  31292  erngplus-rN  31297  erngmul-rN  31300  erngdvlem3  31476  erngdvlem4  31477  erng0g  31480  erngdvlem3-rN  31484  erngdvlem4-rN  31485  dvaplusg  31495  dvamulr  31498  dvavadd  31501  dvavsca  31503  dvalveclem  31512  dvhmulr  31573  dvhfvadd  31578  dvhvadd  31579  dvhopvadd2  31581  dvhvaddcl  31582  dvhvaddcomN  31583  dvhvsca  31588  dvhlveclem  31595  dvh0g  31598  djavalN  31622  diblsmopel  31658  dicvaddcl  31677  cdlemn6  31689  dihffval  31717  dihopelvalcpre  31735  djhval  31885  lcdvaddval  32085  lcdsmul  32089  lcdvsval  32091  lcdlkreq2N  32110  hvmapffval  32245  hvmapfval  32246  hdmap1fval  32284  hgmapffval  32375  hgmapfval  32376  hgmapadd  32384  hlhilipval  32439  hlhilhillem  32450
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-rex 2676  df-uni 3980  df-br 4177  df-iota 5381  df-fv 5425  df-ov 6047
  Copyright terms: Public domain W3C validator