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

Theorem oveqan12d 6059
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 6049 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3syl2an 464 1  |-  ( (
ph  /\  ps )  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649  (class class class)co 6040
This theorem is referenced by:  oveqan12rd  6060  offval  6271  offval3  6277  odi  6781  omopth2  6786  oeoa  6799  ecovdi  6976  ackbij1lem9  8064  alephadd  8408  distrpi  8731  addpipq  8770  mulpipq  8773  lterpq  8803  reclem3pr  8882  mulsrpr  8907  1idsr  8929  mulcnsr  8967  mulid1  9044  1re  9046  mul02  9200  addcom  9208  mulsub  9432  mulsub2  9433  muleqadd  9622  divmuldiv  9670  div2sub  9795  addltmul  10159  xnegdi  10783  xadddilem  10829  fzsubel  11044  fzoval  11096  seqid3  11322  mulexp  11374  sqdiv  11402  hashdom  11608  hashun  11611  ccatfval  11697  splcl  11736  crim  11875  readd  11886  remullem  11888  imadd  11894  cjadd  11901  cjreim  11920  sqrmul  12020  sqabsadd  12042  sqabssub  12043  absmul  12054  abs2dif  12091  binom  12564  sinadd  12720  cosadd  12721  dvds2ln  12835  sadcaddlem  12924  bezoutlem4  12996  bezout  12997  absmulgcd  13002  gcddiv  13004  nn0gcdsq  13099  crt  13122  pythagtriplem1  13145  pcqmul  13182  4sqlem4a  13274  4sqlem4  13275  prdsplusgval  13650  prdsmulrval  13652  prdsdsval  13655  prdsvscaval  13656  xpsfval  13747  xpsval  13752  0mhm  14713  resmhm  14714  prdspjmhm  14721  pwsdiagmhm  14723  gsumws2  14743  frmdup1  14764  eqgval  14944  idghm  14976  resghm  14977  mulgmhm  15405  mulgghm  15406  rnglghm  15666  rngrghm  15667  gsumdixp  15670  isrhm  15779  issrngd  15904  lmodvsghm  15960  asclghm  16352  psrmulfval  16404  evlslem4  16519  xrsdsval  16697  expmhm  16731  expghm  16732  mulgghm2  16741  mulgrhm  16742  cygznlem3  16805  fmval  17928  fmf  17930  flffval  17974  divcn  18851  rescncf  18880  htpyco1  18956  tchcph  19147  volun  19392  dyadval  19437  dvlip  19830  ftc1a  19874  ftc2ditglem  19882  mpfrcl  19892  tdeglem3  19935  q1pval  20029  reefgim  20319  efgh  20396  relogoprlem  20438  eflogeq  20449  lgsdir2  21065  lgsdchr  21085  ghsubgolem  21911  ipasslem11  22294  hhssnv  22717  mayete3i  23183  mayete3iOLD  23184  idunop  23434  idhmop  23438  0lnfn  23441  lnopmi  23456  lnophsi  23457  lnopcoi  23459  hmops  23476  hmopm  23477  nlelshi  23516  cnlnadjlem2  23524  kbass6  23577  strlem3a  23708  hstrlem3a  23716  mndpluscn  24265  xrge0iifhom  24276  rezh  24308  probdsb  24633  zetacvg  24752  rescon  24886  iscvm  24899  ghomsn  25052  binomfallfac  25308  brbtwn2  25748  ax5seglem4  25775  axeuclid  25806  axcontlem2  25808  axcontlem4  25810  axcontlem8  25814  mbfposadd  26153  rrnmval  26427  pellex  26788  rmxfval  26857  rmyfval  26858  qirropth  26861  rmxycomplete  26870  bezoutr1  26941  jm2.15nn0  26964  rmxdioph  26977  expdiophlem2  26983  pwssplit2  27057  mamuval  27312  mamufv  27313  mendvsca  27367  deg1mhm  27394  addrval  27538  subrval  27539  fmulcl  27578  fmuldfeqlem1  27579  dvhopaddN  31597
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator