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

Theorem oveqan12d 5893
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 5883 . 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 1632  (class class class)co 5874
This theorem is referenced by:  oveqan12rd  5894  offval  6101  offval3  6107  odi  6593  omopth2  6598  oeoa  6611  ecovdi  6787  ackbij1lem9  7870  alephadd  8215  distrpi  8538  addpipq  8577  mulpipq  8580  lterpq  8610  reclem3pr  8689  mulsrpr  8714  1idsr  8736  mulcnsr  8774  mulid1  8851  1re  8853  mul02  9006  addcom  9014  mulsub  9238  mulsub2  9239  muleqadd  9428  divmuldiv  9476  div2sub  9601  addltmul  9963  xnegdi  10584  xadddilem  10630  fzsubel  10843  fzoval  10892  seqid3  11106  mulexp  11157  sqdiv  11185  hashdom  11377  hashun  11380  ccatfval  11444  splcl  11483  crim  11616  readd  11627  remullem  11629  imadd  11635  cjadd  11642  cjreim  11661  sqrmul  11761  sqabsadd  11783  sqabssub  11784  absmul  11795  abs2dif  11832  binom  12304  sinadd  12460  cosadd  12461  dvds2ln  12575  sadcaddlem  12664  bezoutlem4  12736  bezout  12737  absmulgcd  12742  gcddiv  12744  nn0gcdsq  12839  crt  12862  pythagtriplem1  12885  pcqmul  12922  4sqlem4a  13014  4sqlem4  13015  prdsplusgval  13388  prdsmulrval  13390  prdsdsval  13393  prdsvscaval  13394  xpsfval  13485  xpsval  13490  0mhm  14451  resmhm  14452  prdspjmhm  14459  pwsdiagmhm  14461  gsumws2  14481  frmdup1  14502  eqgval  14682  idghm  14714  resghm  14715  mulgmhm  15143  mulgghm  15144  rnglghm  15404  rngrghm  15405  gsumdixp  15408  isrhm  15517  issrngd  15642  lmodvsghm  15702  asclghm  16094  psrmulfval  16146  evlslem4  16261  xrsdsval  16431  expmhm  16465  expghm  16466  mulgghm2  16475  mulgrhm  16476  cygznlem3  16539  fmval  17654  fmf  17656  flffval  17700  divcn  18388  rescncf  18417  htpyco1  18492  tchcph  18683  volun  18918  dyadval  18963  dvlip  19356  ftc1a  19400  ftc2ditglem  19408  mpfrcl  19418  tdeglem3  19461  q1pval  19555  reefgim  19842  efgh  19919  relogoprlem  19960  eflogeq  19971  lgsdir2  20583  lgsdchr  20603  ghsubgolem  21053  ipasslem11  21434  hhssnv  21857  mayete3i  22323  mayete3iOLD  22324  idunop  22574  idhmop  22578  0lnfn  22581  lnopmi  22596  lnophsi  22597  lnopcoi  22599  hmops  22616  hmopm  22617  nlelshi  22656  cnlnadjlem2  22664  kbass6  22717  strlem3a  22848  hstrlem3a  22856  mndpluscn  23314  probdsb  23640  zetacvg  23704  rescon  23792  iscvm  23805  ghomsn  24010  brbtwn2  24605  ax5seglem4  24632  axeuclid  24663  axcontlem2  24665  axcontlem4  24667  axcontlem8  24671  rrnmval  26655  pellex  27023  rmxfval  27092  rmyfval  27093  qirropth  27096  rmxycomplete  27105  bezoutr1  27176  jm2.15nn0  27199  rmxdioph  27212  expdiophlem2  27218  pwssplit2  27292  mamuval  27547  mamufv  27548  mendvsca  27602  deg1mhm  27629  addrval  27774  subrval  27775  dvhopaddN  31926
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877
  Copyright terms: Public domain W3C validator