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

Theorem oveq12 6099
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 6097 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 6098 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2493 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1364  (class class class)co 6090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-iota 5378  df-fv 5423  df-ov 6093
This theorem is referenced by:  oveq12i  6102  oveq12d  6108  oveqan12d  6109  sprmpt2d  6741  oev2  6959  oa00  6994  omopthi  7092  ecopoveq  7197  ecopovtrn  7199  th3qlem1  7202  th3qlem2  7203  isfsupp  7620  cantnffval  7865  fpwwe2  8806  halfnq  9141  distrlem5pr  9192  addcmpblnr  9235  addsrpr  9238  mulsrpr  9239  ltsrpr  9240  mulgt0sr  9268  add20  9847  msqge0  9857  recextlem2  9963  cru  10310  zaddcl  10681  qaddcl  10965  qmulcl  10967  xaddval  11189  xmulval  11191  xadddilem  11253  fzopth  11491  modval  11706  1exp  11889  nn0opthi  12044  faclbnd  12062  faclbnd3  12064  bcn0  12082  ccatopth  12360  ccatopth2  12361  repswccat  12419  reval  12591  absval  12723  clim  12968  rlim  12969  fsumparts  13265  cpnnen  13507  dvds2add  13560  dvds2sub  13561  gcddvds  13695  gcdcl  13697  gcdeq0  13701  gcdneg  13706  gcdaddmlem  13708  gcdabs  13713  bezoutlem3  13720  bezout  13722  gcddiv  13729  eucalgval2  13752  isprm5  13794  prmexpb  13799  rpexp  13802  rpmul  13805  nn0gcdsq  13826  opoe  13874  omoe  13875  opeo  13876  omeo  13877  pcqmul  13916  prmreclem3  13975  mul4sq  14011  vdwapval  14030  f1ocpbl  14459  homfval  14627  comfval  14635  issect  14688  isfull  14816  isfth  14820  natfval  14852  catchom  14963  catcco  14965  plusfval  15424  isgim  15783  subgga  15811  cayleylem1  15910  lsmsubm  16145  subgdisjb  16183  pj1fval  16184  odadd1  16323  divsabl  16340  cygabl  16360  dprdsubg  16511  dfrhm2  16798  isrhm  16801  scafval  16947  lss1d  17022  islmhm  17086  islmim  17121  mplval  17479  opsrval  17532  evlval  17586  mpfind  17598  znfld  17952  cygznlem3  17961  cnmsgnsubg  17966  psgnghm  17969  ipeq0  18026  ipfval  18037  dsmmval  18118  dsmmacl  18125  mavmul0g  18323  marrepfval  18330  marrepeval  18333  marepvfval  18335  marepveval  18338  submafval  18349  submaeval  18352  mdetfval  18356  madugsum  18408  minmar1fval  18411  minmar1eval  18414  symgmatr01  18419  gsummatr01lem3  18422  gsummatr01lem4  18423  gsummatr01  18424  tx2ndc  19183  cnmpt2t  19205  cnmpt22f  19207  hmeofval  19290  divstgplem  19650  stdbdmetval  20048  nmofval  20252  nghmfval  20260  isnmhm  20284  xrsxmet  20345  isphtpy  20512  isphtpc  20525  pcorevlem  20557  cphnm  20671  tchnmval  20703  ipcau2  20708  tchcphlem1  20709  tchcphlem2  20710  tchcph  20711  bcthlem1  20794  bcth  20799  dyadmax  21037  volcn  21045  vitalilem1  21047  vitalilem2  21048  vitalilem3  21049  vitali  21052  i1fmullem  21131  itg1addlem4  21136  dvlip  21424  ftc1a  21468  mdegfval  21490  r1pval  21587  coeaddlem  21675  quotval  21717  elqaalem2  21745  taylfval  21783  cxpcn3  22145  resqrcn  22146  sqrcn  22147  abscxpbnd  22150  angval  22156  chordthmlem  22186  dcubic  22200  lgsdchr  22646  mul2sq  22663  ostthlem2  22836  tglngval  22943  wlkon  23364  wlkonprop  23366  trls  23370  trlon  23374  trlonprop  23376  pths  23400  spths  23401  pthon  23409  pthonprop  23411  spthon  23416  spthonprp  23419  isconngra  23493  isconngra1  23494  ablosn  23769  rngo2  23810  hmoval  24145  htth  24255  normval  24461  hlimi  24525  hsn0elch  24586  ocsh  24621  shscli  24655  shs00i  24788  chj00i  24825  riesz4i  25402  stm1addi  25584  stm1add3i  25586  superpos  25693  metidv  26255  rmulccn  26294  pl1cn  26321  sibfof  26656  subfacval2  27005  m1expevenALT  27037  txsconlem  27059  iscvm  27078  ghomgrpilem2  27234  ghomsn  27236  ismblfin  28357  itg2addnclem3  28370  itg2addnc  28371  ftc1anclem3  28394  ftc1anc  28400  bfp  28648  rngohomco  28705  rngoisoval  28708  rngoisocnv  28712  crngohomfo  28731  keridl  28757  ispridlc  28795  mendval  29465  mendplusg  29468  mulvval  29649  fzoopth  30138  wwlkn  30241  is2wlkonot  30307  is2spthonot  30308  2wlkonot  30309  2spthonot  30310  2wlksot  30311  2spthsot  30312  2wlkonot3v  30319  2spthonot3v  30320  clwlk  30343  clwlkcompim  30352  clwwlkn  30355  clwwlknprop  30360  isrgra  30468  mat1dimcrng  30756  dmatmulcl  30762  scmatsubcl  30767  scmatmulcl  30769  lincsumcl  30806  bj-bary1  32325  snatpsubN  33116  cdlemn11pre  34577  dihord2pre  34592  baerlem3lem1  35074
  Copyright terms: Public domain W3C validator