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

Theorem oveq12 6093
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 6091 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 6092 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2490 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653  (class class class)co 6084
This theorem is referenced by:  oveq12i  6096  oveq12d  6102  oveqan12d  6103  sprmpt2  6479  oev2  6770  oa00  6805  omopthi  6903  ecopoveq  7008  ecopovtrn  7010  th3qlem1  7013  th3qlem2  7014  cantnffval  7621  fpwwe2  8523  halfnq  8858  distrlem5pr  8909  addcmpblnr  8952  addsrpr  8955  mulsrpr  8956  ltsrpr  8957  mulgt0sr  8985  add20  9545  msqge0  9554  recextlem2  9658  cru  9997  zaddcl  10322  qaddcl  10595  qmulcl  10597  xaddval  10814  xmulval  10816  xadddilem  10878  fzopth  11094  modval  11257  1exp  11414  nn0opthi  11568  faclbnd  11586  faclbnd3  11588  bcn0  11606  ccatopth  11781  ccatopth2  11782  reval  11916  absval  12048  clim  12293  rlim  12294  fsumparts  12590  cpnnen  12833  dvds2add  12886  dvds2sub  12887  gcddvds  13020  gcdcl  13022  gcdeq0  13026  gcdneg  13031  gcdaddmlem  13033  gcdabs  13038  bezoutlem3  13045  bezout  13047  gcddiv  13054  eucalgval2  13077  isprm5  13117  prmexpb  13122  rpexp  13125  rpmul  13128  nn0gcdsq  13149  opoe  13190  omoe  13191  opeo  13192  omeo  13193  pcqmul  13232  prmreclem3  13291  mul4sq  13327  vdwapval  13346  f1ocpbl  13755  homfval  13923  comfval  13931  issect  13984  isfull  14112  isfth  14116  natfval  14148  catchom  14259  catcco  14261  plusfval  14708  isgim  15054  subgga  15082  cayleylem1  15115  lsmsubm  15292  subgdisjb  15330  pj1fval  15331  odadd1  15468  divsabl  15485  cygabl  15505  dprdsubg  15587  dfrhm2  15826  isrhm  15829  scafval  15974  lss1d  16044  islmhm  16108  islmim  16139  mplval  16497  opsrval  16540  znfld  16846  cygznlem3  16855  ipeq0  16874  ipfval  16885  tx2ndc  17688  cnmpt2t  17710  cnmpt22f  17712  hmeofval  17795  divstgplem  18155  stdbdmetval  18549  nmofval  18753  nghmfval  18761  isnmhm  18785  xrsxmet  18845  isphtpy  19011  isphtpc  19024  pcorevlem  19056  cphnm  19161  tchnmval  19192  ipcau2  19196  tchcphlem1  19197  tchcphlem2  19198  tchcph  19199  bcthlem1  19282  bcth  19287  dyadmax  19495  volcn  19503  vitalilem1  19505  vitalilem2  19506  vitalilem3  19507  vitali  19510  i1fmullem  19589  itg1addlem4  19594  dvlip  19882  ftc1a  19926  evlval  19950  mpfind  19970  mdegfval  19990  r1pval  20084  coeaddlem  20172  quotval  20214  elqaalem2  20242  taylfval  20280  cxpcn3  20637  resqrcn  20638  sqrcn  20639  abscxpbnd  20642  angval  20648  chordthmlem  20678  dcubic  20691  lgsdchr  21137  mul2sq  21154  ostthlem2  21327  wlkon  21535  wlkonprop  21537  trls  21541  trlon  21545  trlonprop  21547  pths  21571  spths  21572  pthon  21580  pthonprop  21582  spthon  21587  spthonprp  21590  isconngra  21664  isconngra1  21665  ablosn  21940  rngo2  21981  hmoval  22316  htth  22426  normval  22631  hlimi  22695  hsn0elch  22755  ocsh  22790  shscli  22824  shs00i  22957  chj00i  22994  riesz4i  23571  stm1addi  23753  stm1add3i  23755  superpos  23862  metidv  24292  rmulccn  24319  sibfof  24659  subfacval2  24878  m1expevenALT  24910  txsconlem  24932  iscvm  24951  ghomgrpilem2  25102  ghomsn  25104  ismblfin  26259  itg2addnclem3  26272  itg2addnc  26273  ftc1anclem3  26296  ftc1anc  26302  bfp  26547  rngohomco  26604  rngoisoval  26607  rngoisocnv  26611  crngohomfo  26630  keridl  26656  ispridlc  26694  dsmmval  27191  dsmmacl  27198  cnmsgnsubg  27425  psgnghm  27428  mdetfval  27478  mendval  27482  mendplusg  27485  mulvval  27663  fzoopth  28162  wwlkn  28364  is2wlkonot  28395  is2spthonot  28396  2wlkonot  28397  2spthonot  28398  2wlksot  28399  2spthsot  28400  2wlkonot3v  28407  2spthonot3v  28408  isrgra  28441  snatpsubN  30621  cdlemn11pre  32082  dihord2pre  32097  baerlem3lem1  32579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-ov 6087
  Copyright terms: Public domain W3C validator