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

Theorem oveqan12d 5877
Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
Hypotheses
Ref Expression
oveq1d.1  |-  ( ph  ->  A  =  B )
opreqan12i.2  |-  ( ps 
->  C  =  D
)
Assertion
Ref Expression
oveqan12d  |-  ( (
ph  /\  ps )  ->  ( A F C )  =  ( B F D ) )

Proof of Theorem oveqan12d
StepHypRef Expression
1 oveq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 opreqan12i.2 . 2  |-  ( ps 
->  C  =  D
)
3 oveq12 5867 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3syl2an 463 1  |-  ( (
ph  /\  ps )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623  (class class class)co 5858
This theorem is referenced by:  oveqan12rd  5878  offval  6085  offval3  6091  odi  6577  omopth2  6582  oeoa  6595  ecovdi  6771  ackbij1lem9  7854  alephadd  8199  distrpi  8522  addpipq  8561  mulpipq  8564  lterpq  8594  reclem3pr  8673  mulsrpr  8698  1idsr  8720  mulcnsr  8758  mulid1  8835  1re  8837  mul02  8990  addcom  8998  mulsub  9222  mulsub2  9223  muleqadd  9412  divmuldiv  9460  div2sub  9585  addltmul  9947  xnegdi  10568  xadddilem  10614  fzsubel  10827  fzoval  10876  seqid3  11090  mulexp  11141  sqdiv  11169  hashdom  11361  hashun  11364  ccatfval  11428  splcl  11467  crim  11600  readd  11611  remullem  11613  imadd  11619  cjadd  11626  cjreim  11645  sqrmul  11745  sqabsadd  11767  sqabssub  11768  absmul  11779  abs2dif  11816  binom  12288  sinadd  12444  cosadd  12445  dvds2ln  12559  sadcaddlem  12648  bezoutlem4  12720  bezout  12721  absmulgcd  12726  gcddiv  12728  nn0gcdsq  12823  crt  12846  pythagtriplem1  12869  pcqmul  12906  4sqlem4a  12998  4sqlem4  12999  prdsplusgval  13372  prdsmulrval  13374  prdsdsval  13377  prdsvscaval  13378  xpsfval  13469  xpsval  13474  0mhm  14435  resmhm  14436  prdspjmhm  14443  pwsdiagmhm  14445  gsumws2  14465  frmdup1  14486  eqgval  14666  idghm  14698  resghm  14699  mulgmhm  15127  mulgghm  15128  rnglghm  15388  rngrghm  15389  gsumdixp  15392  isrhm  15501  issrngd  15626  lmodvsghm  15686  asclghm  16078  psrmulfval  16130  evlslem4  16245  xrsdsval  16415  expmhm  16449  expghm  16450  mulgghm2  16459  mulgrhm  16460  cygznlem3  16523  fmval  17638  fmf  17640  flffval  17684  divcn  18372  rescncf  18401  htpyco1  18476  tchcph  18667  volun  18902  dyadval  18947  dvlip  19340  ftc1a  19384  ftc2ditglem  19392  mpfrcl  19402  tdeglem3  19445  q1pval  19539  reefgim  19826  efgh  19903  relogoprlem  19944  eflogeq  19955  lgsdir2  20567  lgsdchr  20587  ghsubgolem  21037  ipasslem11  21418  hhssnv  21841  mayete3i  22307  mayete3iOLD  22308  idunop  22558  idhmop  22562  0lnfn  22565  lnopmi  22580  lnophsi  22581  lnopcoi  22583  hmops  22600  hmopm  22601  nlelshi  22640  cnlnadjlem2  22648  kbass6  22701  strlem3a  22832  hstrlem3a  22840  mndpluscn  23299  probdsb  23625  zetacvg  23689  rescon  23777  iscvm  23790  ghomsn  23995  brbtwn2  24533  ax5seglem4  24560  axeuclid  24591  axcontlem2  24593  axcontlem4  24595  axcontlem8  24599  rrnmval  26552  pellex  26920  rmxfval  26989  rmyfval  26990  qirropth  26993  rmxycomplete  27002  bezoutr1  27073  jm2.15nn0  27096  rmxdioph  27109  expdiophlem2  27115  pwssplit2  27189  mamuval  27444  mamufv  27445  mendvsca  27499  deg1mhm  27526  addrval  27671  subrval  27672  dvhopaddN  31304
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator