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

Theorem oveq12 6082
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 6080 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
2 oveq2 6081 . 2  |-  ( C  =  D  ->  ( B F C )  =  ( B F D ) )
31, 2sylan9eq 2487 1  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652  (class class class)co 6073
This theorem is referenced by:  oveq12i  6085  oveq12d  6091  oveqan12d  6092  sprmpt2  6468  oev2  6759  oa00  6794  omopthi  6892  ecopoveq  6997  ecopovtrn  6999  th3qlem1  7002  th3qlem2  7003  cantnffval  7608  fpwwe2  8508  halfnq  8843  distrlem5pr  8894  addcmpblnr  8937  addsrpr  8940  mulsrpr  8941  ltsrpr  8942  mulgt0sr  8970  add20  9530  msqge0  9539  recextlem2  9643  cru  9982  zaddcl  10307  qaddcl  10580  qmulcl  10582  xaddval  10799  xmulval  10801  xadddilem  10863  fzopth  11079  modval  11242  1exp  11399  nn0opthi  11553  faclbnd  11571  faclbnd3  11573  bcn0  11591  ccatopth  11766  ccatopth2  11767  reval  11901  absval  12033  clim  12278  rlim  12279  fsumparts  12575  cpnnen  12818  dvds2add  12871  dvds2sub  12872  gcddvds  13005  gcdcl  13007  gcdeq0  13011  gcdneg  13016  gcdaddmlem  13018  gcdabs  13023  bezoutlem3  13030  bezout  13032  gcddiv  13039  eucalgval2  13062  isprm5  13102  prmexpb  13107  rpexp  13110  rpmul  13113  nn0gcdsq  13134  opoe  13175  omoe  13176  opeo  13177  omeo  13178  pcqmul  13217  prmreclem3  13276  mul4sq  13312  vdwapval  13331  f1ocpbl  13740  homfval  13908  comfval  13916  issect  13969  isfull  14097  isfth  14101  natfval  14133  catchom  14244  catcco  14246  plusfval  14693  isgim  15039  subgga  15067  cayleylem1  15100  lsmsubm  15277  subgdisjb  15315  pj1fval  15316  odadd1  15453  divsabl  15470  cygabl  15490  dprdsubg  15572  dfrhm2  15811  isrhm  15814  scafval  15959  lss1d  16029  islmhm  16093  islmim  16124  mplval  16482  opsrval  16525  znfld  16831  cygznlem3  16840  ipeq0  16859  ipfval  16870  tx2ndc  17673  cnmpt2t  17695  cnmpt22f  17697  hmeofval  17780  divstgplem  18140  stdbdmetval  18534  nmofval  18738  nghmfval  18746  isnmhm  18770  xrsxmet  18830  isphtpy  18996  isphtpc  19009  pcorevlem  19041  cphnm  19146  tchnmval  19177  ipcau2  19181  tchcphlem1  19182  tchcphlem2  19183  tchcph  19184  bcthlem1  19267  bcth  19272  dyadmax  19480  volcn  19488  vitalilem1  19490  vitalilem2  19491  vitalilem3  19492  vitali  19495  i1fmullem  19576  itg1addlem4  19581  dvlip  19867  ftc1a  19911  evlval  19935  mpfind  19955  mdegfval  19975  r1pval  20069  coeaddlem  20157  quotval  20199  elqaalem2  20227  taylfval  20265  cxpcn3  20622  resqrcn  20623  sqrcn  20624  abscxpbnd  20627  angval  20633  chordthmlem  20663  dcubic  20676  lgsdchr  21122  mul2sq  21139  ostthlem2  21312  wlkon  21520  wlkonprop  21522  trls  21526  trlon  21530  trlonprop  21532  pths  21556  spths  21557  pthon  21565  pthonprop  21567  spthon  21572  spthonprp  21575  isconngra  21649  isconngra1  21650  ablosn  21925  rngo2  21966  hmoval  22301  htth  22411  normval  22616  hlimi  22680  hsn0elch  22740  ocsh  22775  shscli  22809  shs00i  22942  chj00i  22979  riesz4i  23556  stm1addi  23738  stm1add3i  23740  superpos  23847  metidv  24277  rmulccn  24304  sibfof  24644  subfacval2  24863  m1expevenALT  24895  txsconlem  24917  iscvm  24936  ghomgrpilem2  25087  ghomsn  25089  ismblfin  26210  itg2addnclem3  26221  itg2addnc  26222  bfp  26487  rngohomco  26544  rngoisoval  26547  rngoisocnv  26551  crngohomfo  26570  keridl  26596  ispridlc  26634  dsmmval  27132  dsmmacl  27139  cnmsgnsubg  27366  psgnghm  27369  mdetfval  27419  mendval  27423  mendplusg  27426  mulvval  27604  is2wlkonot  28247  is2spthonot  28248  2wlkonot  28249  2spthonot  28250  2wlksot  28251  2spthsot  28252  2wlkonot3v  28259  2spthonot3v  28260  snatpsubN  30448  cdlemn11pre  31909  dihord2pre  31924  baerlem3lem1  32406
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076
  Copyright terms: Public domain W3C validator