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

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

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 7152 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
2 oveq2 7153 . 2 (𝐶 = 𝐷 → (𝐵𝐹𝐶) = (𝐵𝐹𝐷))
31, 2sylan9eq 2873 1 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  (class class class)co 7145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  oveq12i  7157  oveq12d  7163  oveqan12d  7164  mptmpoopabovd  7768  suppofssd  7856  sprmpod  7879  oev2  8137  oa00  8174  omopthi  8273  ecopoveq  8387  ecopovtrn  8389  isfsupp  8825  cantnffval  9114  fpwwe2  10053  halfnq  10386  distrlem5pr  10437  addcmpblnr  10479  ltsrpr  10487  mulgt0sr  10515  add20  11140  msqge0  11149  recextlem2  11259  cru  11618  zaddcl  12010  qaddcl  12352  qmulcl  12354  xaddval  12604  xmulval  12606  xnn0xadd0  12628  xadddilem  12675  fzopth  12932  modval  13227  1exp  13446  m1expeven  13464  nn0opthi  13618  faclbnd  13638  faclbnd3  13640  bcn0  13658  ccatopth  14066  ccatopth2  14067  repswccat  14136  reval  14453  absval  14585  clim  14839  rlim  14840  fsumparts  15149  cpnnen  15570  dvds2add  15631  dvds2sub  15632  opoe  15700  omoe  15701  opeo  15702  omeo  15703  gcddvds  15840  gcdcl  15843  gcdeq0  15853  gcdneg  15858  gcdaddmlem  15860  gcdabs  15865  bezoutlem3  15877  bezout  15879  gcddiv  15887  eucalgval2  15913  lcmabs  15937  rpmul  15991  divgcdcoprmex  15998  isprm5  16039  prmexpb  16050  rpexp  16052  nn0gcdsq  16080  pcqmul  16178  prmreclem3  16242  mul4sq  16278  vdwapval  16297  f1ocpbl  16786  homfval  16950  comfval  16958  issect  17011  isfull  17168  isfth  17172  natfval  17204  catchom  17347  catcco  17349  funcsetcestrclem5  17397  plusfval  17847  0subm  17970  cycsubm  18283  cyccom  18284  isgim  18340  subgga  18368  cayleylem1  18469  lsmsubm  18707  subgdisjb  18748  pj1fval  18749  odadd1  18897  qusabl  18914  cygablOLD  18940  dprdsubg  19075  ringadd2  19254  dfrhm2  19398  isrhm  19402  isrim0  19404  scafval  19582  rmodislmodlem  19630  rmodislmod  19631  lss1d  19664  islmhm  19728  islmim  19763  mplval  20136  mplcoe5lem  20176  opsrval  20183  evlval  20236  mpfind  20248  selvffval  20257  mhpfval  20260  znfld  20635  cygznlem3  20644  cnmsgnsubg  20649  psgnghm  20652  ipeq0  20710  ipfval  20721  dsmmval  20806  dsmmacl  20813  mat1dimcrng  21014  dmatval  21029  dmatmulcl  21037  scmatval  21041  scmataddcl  21053  scmatsubcl  21054  scmatmulcl  21055  mavmul0g  21090  marrepfval  21097  marrepeval  21100  marepvfval  21102  marepveval  21105  submafval  21116  submaeval  21119  mdetfval  21123  madugsum  21180  minmar1fval  21183  minmar1eval  21186  symgmatr01  21191  gsummatr01lem3  21194  gsummatr01lem4  21195  gsummatr01  21196  cpmatacl  21252  mat2pmatfval  21259  mat2pmatvalel  21261  mat2pmatmul  21267  cpm2mfval  21285  cpm2mvalel  21287  m2cpminvid  21289  m2cpminvid2  21291  decpmate  21302  pmatcollpw1  21312  monmatcollpw  21315  pmatcollpwlem  21316  pmatcollpw  21317  pmatcollpwscmatlem2  21326  pm2mpval  21331  pm2mpf1  21335  mp2pm2mplem3  21344  mp2pm2mplem4  21345  chpmatfval  21366  tx2ndc  22187  cnmpt2t  22209  cnmpt22f  22211  hmeofval  22294  qustgplem  22656  stdbdmetval  23051  nmofval  23250  nghmfval  23258  isnmhm  23282  xrsxmet  23344  isphtpy  23512  isphtpc  23525  pcorevlem  23557  cphnm  23724  tcphnmval  23759  ipcau2  23764  tcphcphlem1  23765  tcphcphlem2  23766  tcphcph  23767  bcthlem1  23854  bcth  23859  dyadmax  24126  volcn  24134  vitalilem1  24136  vitalilem2  24137  vitalilem3  24138  vitali  24141  i1fmullem  24222  itg1addlem4  24227  dvlip  24517  ftc1a  24561  mdegfval  24583  r1pval  24677  coeaddlem  24766  quotval  24808  elqaalem2  24836  taylfval  24874  cxpcn3  25256  resqrtcn  25257  sqrtcn  25258  abscxpbnd  25261  angval  25306  chordthmlem  25337  dcubic  25351  lgsdchr  25858  mul2sq  25922  ostthlem2  26131  tglngval  26264  islnopp  26452  ishpg  26472  finsumvtxdg2size  27259  wspthsn  27553  wwlksnon  27556  wspthsnon  27557  iswspthsnon  27561  2clwwlk  28053  numclwlk1lem2  28076  numclwwlkovh0  28078  hmoval  28514  htth  28622  normval  28828  hlimi  28892  hsn0elch  28952  ocsh  28987  shscli  29021  shs00i  29154  chj00i  29191  riesz4i  29767  stm1addi  29949  stm1add3i  29951  superpos  30058  brfinext  30942  submateq  30973  metidv  31031  rmulccn  31070  pl1cn  31097  sibfof  31497  cxpcncf1  31765  subfacval2  32331  txsconnlem  32384  iscvm  32403  prv  32572  bj-bary1  34481  ismblfin  34814  itg2addnclem3  34826  itg2addnc  34827  ftc1anclem3  34850  ftc1anc  34856  bfp  34983  rngo2  35066  rngohomco  35133  rngoisoval  35136  rngoisocnv  35140  crngohomfo  35165  keridl  35191  ispridlc  35229  snatpsubN  36766  cdlemn11pre  38226  dihord2pre  38241  baerlem3lem1  38723  nn0rppwr  39060  mendval  39661  mendplusg  39664  mulvval  40677  climf  41779  climf2  41823  cxpcncf2  42059  smflimlem3  42926  fzoopth  43404  fmtnofac2lem  43607  prmdvdsfmtnof1lem2  43624  opoeALTV  43725  opeoALTV  43726  rnghmval  44090  isrngisom  44095  rhmval  44118  rngchomALTV  44184  funcrngcsetcALT  44198  funcringcsetcALTV2lem5  44239  ringchomALTV  44247  funcringcsetclem5ALTV  44262  srhmsubclem3  44274  srhmsubc  44275  fldhmsubc  44283  srhmsubcALTVlem2  44292  srhmsubcALTV  44293  fldhmsubcALTV  44301  dmatALTval  44383  lincsumcl  44414  fdivval  44527
  Copyright terms: Public domain W3C validator