MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveq12 Structured version   Visualization version   GIF version

Theorem oveq12 7362
Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
Assertion
Ref Expression
oveq12 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 7360 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2 oveq2 7361 . 2 (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
31, 2sylan9eq 2796 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  (class class class)co 7353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-iota 6445  df-fv 6501  df-ov 7356
This theorem is referenced by:  oveq12i  7365  oveq12d  7371  oveqan12d  7372  mptmpoopabovd  8010  mptmpoopabovdOLD  8012  suppofssd  8130  sprmpod  8151  oev2  8465  oa00  8502  omopthi  8603  ecopoveq  8753  ecopovtrn  8755  isfsupp  9305  cantnffval  9595  ttrcltr  9648  fpwwe2  10575  halfnq  10908  distrlem5pr  10959  addcmpblnr  11001  ltsrpr  11009  mulgt0sr  11037  add20  11663  msqge0  11672  recextlem2  11782  cru  12141  zaddcl  12539  qaddcl  12882  qmulcl  12884  xaddval  13134  xmulval  13136  xnn0xadd0  13158  xadddilem  13205  fzopth  13470  modval  13768  1exp  13989  m1expeven  14007  nn0opthi  14162  faclbnd  14182  faclbnd3  14184  bcn0  14202  ccatopth  14596  ccatopth2  14597  repswccat  14666  reval  14983  absval  15115  clim  15368  rlim  15369  fsumparts  15683  cpnnen  16103  dvds2add  16164  dvds2sub  16165  opoe  16237  omoe  16238  opeo  16239  omeo  16240  gcddvds  16375  gcdcl  16378  gcdeq0  16389  gcdneg  16394  gcdaddmlem  16396  gcdabsOLD  16404  bezoutlem3  16414  bezout  16416  gcddiv  16424  eucalgval2  16449  lcmabs  16473  rpmul  16527  divgcdcoprmex  16534  isprm5  16575  prmexpb  16588  rpexp  16590  nn0gcdsq  16619  pcqmul  16717  prmreclem3  16782  mul4sq  16818  vdwapval  16837  f1ocpbl  17399  homfval  17564  comfval  17572  issect  17628  isfull  17789  isfth  17793  natfval  17825  catchom  17981  catcco  17983  funcsetcestrclem5  18039  plusfval  18496  0subm  18620  cycsubm  18986  cyccom  18987  isgim  19043  subgga  19071  cayleylem1  19185  lsmsubm  19426  subgdisjb  19466  pj1fval  19467  odadd1  19617  qusabl  19634  dprdsubg  19794  ringadd2  19982  dfrhm2  20133  isrhm  20137  isrim0OLD  20139  isrim0  20141  scafval  20326  rmodislmodlem  20374  rmodislmod  20375  rmodislmodOLD  20376  lss1d  20409  islmhm  20473  islmim  20508  znfld  20952  cygznlem3  20961  cnmsgnsubg  20966  psgnghm  20969  ipeq0  21027  ipfval  21038  dsmmval  21125  dsmmacl  21132  mplval  21381  mplcoe5lem  21424  opsrval  21431  evlval  21489  mpfind  21501  selvffval  21510  mhpfval  21513  mhpmulcl  21523  mat1dimcrng  21810  dmatval  21825  dmatmulcl  21833  scmatval  21837  scmataddcl  21849  scmatsubcl  21850  scmatmulcl  21851  mavmul0g  21886  marrepfval  21893  marrepeval  21896  marepvfval  21898  marepveval  21901  submafval  21912  submaeval  21915  mdetfval  21919  madugsum  21976  minmar1fval  21979  minmar1eval  21982  symgmatr01  21987  gsummatr01lem3  21990  gsummatr01lem4  21991  gsummatr01  21992  cpmatacl  22049  mat2pmatfval  22056  mat2pmatvalel  22058  mat2pmatmul  22064  cpm2mfval  22082  cpm2mvalel  22084  m2cpminvid  22086  m2cpminvid2  22088  decpmate  22099  pmatcollpw1  22109  monmatcollpw  22112  pmatcollpwlem  22113  pmatcollpw  22114  pmatcollpwscmatlem2  22123  pm2mpval  22128  pm2mpf1  22132  mp2pm2mplem3  22141  mp2pm2mplem4  22142  chpmatfval  22163  tx2ndc  22986  cnmpt2t  23008  cnmpt22f  23010  hmeofval  23093  qustgplem  23456  stdbdmetval  23854  nmofval  24062  nghmfval  24070  isnmhm  24094  xrsxmet  24156  isphtpy  24328  isphtpc  24341  pcorevlem  24373  cphnm  24541  tcphnmval  24577  ipcau2  24582  tcphcphlem1  24583  tcphcphlem2  24584  tcphcph  24585  bcthlem1  24672  bcth  24677  dyadmax  24946  volcn  24954  vitalilem1  24956  vitalilem2  24957  vitalilem3  24958  vitali  24961  i1fmullem  25042  itg1addlem4  25047  itg1addlem4OLD  25048  dvlip  25341  ftc1a  25385  mdegfval  25411  r1pval  25505  coeaddlem  25594  quotval  25636  elqaalem2  25664  taylfval  25702  cxpcn3  26085  resqrtcn  26086  sqrtcn  26087  abscxpbnd  26090  angval  26135  chordthmlem  26166  dcubic  26180  lgsdchr  26687  mul2sq  26751  ostthlem2  26960  tglngval  27379  islnopp  27567  ishpg  27587  finsumvtxdg2size  28384  wspthsn  28679  wwlksnon  28682  wspthsnon  28683  iswspthsnon  28687  2clwwlk  29177  numclwlk1lem2  29200  numclwwlkovh0  29202  hmoval  29638  htth  29746  normval  29952  hlimi  30016  hsn0elch  30076  ocsh  30111  shscli  30145  shs00i  30278  chj00i  30315  riesz4i  30891  stm1addi  31073  stm1add3i  31075  superpos  31182  prmidlc  32100  idlsrgmulrval  32130  brfinext  32219  irngval  32236  submateq  32259  metidv  32342  rmulccn  32378  pl1cn  32405  sibfof  32809  cxpcncf1  33077  subfacval2  33650  txsconnlem  33703  iscvm  33722  prv  33891  bj-bary1  35750  ismblfin  36086  itg2addnclem3  36098  itg2addnc  36099  ftc1anclem3  36120  ftc1anc  36126  bfp  36250  rngo2  36333  rngohomco  36400  rngoisoval  36403  rngoisocnv  36407  crngohomfo  36432  keridl  36458  ispridlc  36496  snatpsubN  38180  cdlemn11pre  39640  dihord2pre  39655  baerlem3lem1  40137  nn0rppwr  40757  sn-inelr  40872  prjcrvfval  40907  mendval  41448  mendplusg  41451  omcl3g  41605  mulvval  42690  climf  43795  climf2  43839  cxpcncf2  44072  smflimlem3  44946  fzoopth  45491  fmtnofac2lem  45692  prmdvdsfmtnof1lem2  45709  opoeALTV  45807  opeoALTV  45808  rnghmval  46121  isrngisom  46126  rhmval  46149  rngchomALTV  46215  funcrngcsetcALT  46229  funcringcsetcALTV2lem5  46270  ringchomALTV  46278  funcringcsetclem5ALTV  46293  srhmsubclem3  46305  srhmsubc  46306  fldhmsubc  46314  srhmsubcALTVlem2  46323  srhmsubcALTV  46324  fldhmsubcALTV  46332  dmatALTval  46413  lincsumcl  46444  fdivval  46557  catprslem  46962  catprsc  46965  catprsc2  46966  thincmoALT  46982  functhinclem2  46994  fullthinc2  46999
  Copyright terms: Public domain W3C validator