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

Theorem oveqan12d 6102
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 6092 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3syl2an 465 1  |-  ( (
ph  /\  ps )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653  (class class class)co 6083
This theorem is referenced by:  oveqan12rd  6103  offval  6314  offval3  6320  odi  6824  omopth2  6829  oeoa  6842  ecovdi  7019  ackbij1lem9  8110  alephadd  8454  distrpi  8777  addpipq  8816  mulpipq  8819  lterpq  8849  reclem3pr  8928  mulsrpr  8953  1idsr  8975  mulcnsr  9013  mulid1  9090  1re  9092  mul02  9246  addcom  9254  mulsub  9478  mulsub2  9479  muleqadd  9668  divmuldiv  9716  div2sub  9841  addltmul  10205  xnegdi  10829  xadddilem  10875  fzsubel  11090  fzoval  11143  seqid3  11369  mulexp  11421  sqdiv  11449  hashdom  11655  hashun  11658  ccatfval  11744  splcl  11783  crim  11922  readd  11933  remullem  11935  imadd  11941  cjadd  11948  cjreim  11967  sqrmul  12067  sqabsadd  12089  sqabssub  12090  absmul  12101  abs2dif  12138  binom  12611  sinadd  12767  cosadd  12768  dvds2ln  12882  sadcaddlem  12971  bezoutlem4  13043  bezout  13044  absmulgcd  13049  gcddiv  13051  nn0gcdsq  13146  crt  13169  pythagtriplem1  13192  pcqmul  13229  4sqlem4a  13321  4sqlem4  13322  prdsplusgval  13697  prdsmulrval  13699  prdsdsval  13702  prdsvscaval  13703  xpsfval  13794  xpsval  13799  0mhm  14760  resmhm  14761  prdspjmhm  14768  pwsdiagmhm  14770  gsumws2  14790  frmdup1  14811  eqgval  14991  idghm  15023  resghm  15024  mulgmhm  15452  mulgghm  15453  rnglghm  15713  rngrghm  15714  gsumdixp  15717  isrhm  15826  issrngd  15951  lmodvsghm  16007  asclghm  16399  psrmulfval  16451  evlslem4  16566  xrsdsval  16744  expmhm  16778  expghm  16779  mulgghm2  16788  mulgrhm  16789  cygznlem3  16852  fmval  17977  fmf  17979  flffval  18023  divcn  18900  rescncf  18929  htpyco1  19005  tchcph  19196  volun  19441  dyadval  19486  dvlip  19879  ftc1a  19923  ftc2ditglem  19931  mpfrcl  19941  tdeglem3  19984  q1pval  20078  reefgim  20368  efgh  20445  relogoprlem  20487  eflogeq  20498  lgsdir2  21114  lgsdchr  21134  ghsubgolem  21960  ipasslem11  22343  hhssnv  22766  mayete3i  23232  mayete3iOLD  23233  idunop  23483  idhmop  23487  0lnfn  23490  lnopmi  23505  lnophsi  23506  lnopcoi  23508  hmops  23525  hmopm  23526  nlelshi  23565  cnlnadjlem2  23573  kbass6  23626  strlem3a  23757  hstrlem3a  23765  mndpluscn  24314  xrge0iifhom  24325  rezh  24357  probdsb  24682  zetacvg  24801  rescon  24935  iscvm  24948  ghomsn  25101  binomfallfac  25359  brbtwn2  25846  ax5seglem4  25873  axeuclid  25904  axcontlem2  25906  axcontlem4  25908  axcontlem8  25912  mbfposadd  26256  ftc1anclem3  26284  rrnmval  26539  pellex  26900  rmxfval  26969  rmyfval  26970  qirropth  26973  rmxycomplete  26982  bezoutr1  27053  jm2.15nn0  27076  rmxdioph  27089  expdiophlem2  27095  pwssplit2  27168  mamuval  27423  mamufv  27424  mendvsca  27478  deg1mhm  27505  addrval  27649  subrval  27650  fmulcl  27689  fmuldfeqlem1  27690  dvhopaddN  31974
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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 4215  df-iota 5420  df-fv 5464  df-ov 6086
  Copyright terms: Public domain W3C validator