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

Theorem oveq12 6317
Description: Equality theorem for operation value. (Contributed by NM, 16-Jul-1995.)
Assertion
Ref Expression
oveq12  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )

Proof of Theorem oveq12
StepHypRef Expression
1 oveq1 6315 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 6316 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2525 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    = wceq 1452  (class class class)co 6308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-iota 5553  df-fv 5597  df-ov 6311
This theorem is referenced by:  oveq12i  6320  oveq12d  6326  oveqan12d  6327  sprmpt2d  6989  oev2  7243  oa00  7278  omopthi  7376  ecopoveq  7482  ecopovtrn  7484  isfsupp  7905  cantnffval  8186  fpwwe2  9086  halfnq  9419  distrlem5pr  9470  addcmpblnr  9511  ltsrpr  9519  mulgt0sr  9547  add20  10147  msqge0  10156  recextlem2  10265  cru  10623  zaddcl  11001  qaddcl  11303  qmulcl  11305  xaddval  11539  xmulval  11541  xadddilem  11605  fzopth  11861  modval  12131  1exp  12339  m1expeven  12357  nn0opthi  12494  faclbnd  12513  faclbnd3  12515  bcn0  12533  ccatopth  12880  ccatopth2  12881  repswccat  12942  reval  13246  absval  13378  clim  13635  rlim  13636  fsumparts  13943  cpnnen  14358  dvds2add  14411  dvds2sub  14412  gcddvds  14556  gcdcl  14559  gcdeq0  14564  gcdneg  14569  gcdaddmlem  14571  gcdabs  14576  bezoutlem3OLD  14584  bezoutlem3  14587  bezout  14589  gcddiv  14596  eucalgval2  14619  lcmabs  14649  isprm5  14730  prmexpb  14749  rpexp  14751  rpmul  14754  nn0gcdsq  14780  opoe  14840  omoe  14841  opeo  14842  omeo  14843  pcqmul  14882  prmreclem3  14941  mul4sq  14977  vdwapval  15002  f1ocpbl  15509  homfval  15675  comfval  15683  issect  15736  isfull  15893  isfth  15897  natfval  15929  catchom  16072  catcco  16074  funcsetcestrclem5  16122  plusfval  16572  isgim  17004  subgga  17032  cayleylem1  17131  lsmsubm  17383  subgdisjb  17421  pj1fval  17422  odadd1  17564  qusabl  17581  cygabl  17603  dprdsubg  17735  dfrhm2  18023  isrhm  18027  isrim0  18029  scafval  18188  lss1d  18264  islmhm  18328  islmim  18363  mplval  18729  mplcoe5lem  18768  opsrval  18775  evlval  18824  mpfind  18836  znfld  19208  cygznlem3  19217  cnmsgnsubg  19222  psgnghm  19225  ipeq0  19282  ipfval  19293  dsmmval  19374  dsmmacl  19381  mat1dimcrng  19579  dmatval  19594  dmatmulcl  19602  scmatval  19606  scmataddcl  19618  scmatsubcl  19619  scmatmulcl  19620  mavmul0g  19655  marrepfval  19662  marrepeval  19665  marepvfval  19667  marepveval  19670  submafval  19681  submaeval  19684  mdetfval  19688  madugsum  19745  minmar1fval  19748  minmar1eval  19751  symgmatr01  19756  gsummatr01lem3  19759  gsummatr01lem4  19760  gsummatr01  19761  cpmatacl  19817  mat2pmatfval  19824  mat2pmatvalel  19826  mat2pmatmul  19832  cpm2mfval  19850  cpm2mvalel  19852  m2cpminvid  19854  m2cpminvid2  19856  decpmate  19867  pmatcollpw1  19877  monmatcollpw  19880  pmatcollpwlem  19881  pmatcollpw  19882  pmatcollpwscmatlem2  19891  pm2mpval  19896  pm2mpf1  19900  mp2pm2mplem3  19909  mp2pm2mplem4  19910  chpmatfval  19931  tx2ndc  20743  cnmpt2t  20765  cnmpt22f  20767  hmeofval  20850  qustgplem  21213  stdbdmetval  21607  nmofval  21797  nghmfval  21805  nmofvalOLD  21816  nghmfvalOLD  21823  isnmhm  21845  xrsxmet  21905  isphtpy  22090  isphtpc  22103  pcorevlem  22135  cphnm  22249  tchnmval  22281  ipcau2  22286  tchcphlem1  22287  tchcphlem2  22288  tchcph  22289  bcthlem1  22370  bcth  22375  dyadmax  22635  volcn  22643  vitalilem1  22645  vitalilem2  22646  vitalilem3  22647  vitali  22650  i1fmullem  22731  itg1addlem4  22736  dvlip  23024  ftc1a  23068  mdegfval  23090  r1pval  23186  coeaddlem  23282  quotval  23324  elqaalem2  23352  elqaalem2OLD  23355  taylfval  23393  cxpcn3  23767  resqrtcn  23768  sqrtcn  23769  abscxpbnd  23772  angval  23809  chordthmlem  23837  dcubic  23851  lgsdchr  24355  mul2sq  24372  ostthlem2  24545  tglngval  24675  islnopp  24860  ishpg  24880  wlkon  25340  wlkonprop  25342  trls  25345  trlon  25349  trlonprop  25351  pths  25375  spths  25376  pthon  25384  pthonprop  25386  spthon  25391  spthonprp  25394  isconngra  25479  isconngra1  25480  wwlkn  25489  clwlk  25560  clwlkcompim  25571  clwwlkn  25574  clwwlknprop  25579  is2wlkonot  25670  is2spthonot  25671  2wlkonot  25672  2spthonot  25673  2wlksot  25674  2spthsot  25675  2wlkonot3v  25682  2spthonot3v  25683  isrgra  25733  ablosn  26156  rngo2  26197  hmoval  26532  htth  26652  normval  26858  hlimi  26922  hsn0elch  26982  ocsh  27017  shscli  27051  shs00i  27184  chj00i  27221  riesz4i  27797  stm1addi  27979  stm1add3i  27981  superpos  28088  submateq  28709  metidv  28769  rmulccn  28808  pl1cn  28835  sibfof  29246  subfacval2  29982  txsconlem  30035  iscvm  30054  ghomgrpilem2  30376  ghomsn  30378  bj-bary1  31787  ismblfin  32045  itg2addnclem3  32059  itg2addnc  32060  ftc1anclem3  32083  ftc1anc  32089  bfp  32220  rngohomco  32277  rngoisoval  32280  rngoisocnv  32284  crngohomfo  32303  keridl  32329  ispridlc  32367  snatpsubN  33386  cdlemn11pre  34849  dihord2pre  34864  baerlem3lem1  35346  mendval  36120  mendplusg  36123  mulvval  36891  climf  37799  cxpcncf2  37875  opoeALTV  38957  opeoALTV  38958  mptmpt2opabovd  39181  fzoopth  39208  xnn0xadd0  39238  rnghmval  40399  isrngisom  40404  rhmval  40427  rngchomALTV  40495  funcrngcsetcALT  40509  funcringcsetcALTV2lem5  40550  ringchomALTV  40558  funcringcsetclem5ALTV  40573  srhmsubclem3  40585  srhmsubc  40586  fldhmsubc  40594  srhmsubcALTVlem3  40604  srhmsubcALTV  40605  fldhmsubcALTV  40613  dmatALTval  40701  lincsumcl  40732  fdivval  40858
  Copyright terms: Public domain W3C validator