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

Theorem oveqan12d 6893
Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)
Hypotheses
Ref Expression
oveq1d.1 (𝜑𝐴 = 𝐵)
opreqan12i.2 (𝜓𝐶 = 𝐷)
Assertion
Ref Expression
oveqan12d ((𝜑𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveqan12d
StepHypRef Expression
1 oveq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 opreqan12i.2 . 2 (𝜓𝐶 = 𝐷)
3 oveq12 6883 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3syl2an 585 1 ((𝜑𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  (class class class)co 6874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6064  df-fv 6109  df-ov 6877
This theorem is referenced by:  oveqan12rd  6894  offval  7134  offval3  7392  odi  7896  omopth2  7901  oeoa  7914  ecovdi  8091  ackbij1lem9  9335  alephadd  9684  distrpi  10005  addpipq  10044  mulpipq  10047  lterpq  10077  reclem3pr  10156  1idsr  10204  mulcnsr  10242  mulid1  10323  1re  10325  mul02  10499  addcom  10507  mulsub  10758  mulsub2  10759  muleqadd  10956  divmuldiv  11010  div2sub  11135  addltmul  11535  xnegdi  12296  xadddilem  12342  fzsubel  12600  fzoval  12695  seqid3  13068  mulexp  13122  sqdiv  13151  hashdom  13386  hashun  13389  ccatfval  13570  splcl  13727  crim  14078  readd  14089  remullem  14091  imadd  14097  cjadd  14104  cjreim  14123  sqrtmul  14223  sqabsadd  14245  sqabssub  14246  absmul  14257  abs2dif  14295  binom  14784  binomfallfac  14992  sinadd  15114  cosadd  15115  dvds2ln  15237  sadcaddlem  15398  bezoutlem4  15478  bezout  15479  absmulgcd  15485  gcddiv  15487  bezoutr1  15501  lcmgcd  15539  lcmfass  15578  nn0gcdsq  15677  crth  15700  pythagtriplem1  15738  pcqmul  15775  4sqlem4a  15872  4sqlem4  15873  prdsplusgval  16338  prdsmulrval  16340  prdsdsval  16343  prdsvscaval  16344  xpsfval  16432  xpsval  16437  idmhm  17549  0mhm  17563  resmhm  17564  prdspjmhm  17572  pwsdiagmhm  17574  gsumws2  17584  frmdup1  17606  eqgval  17845  idghm  17877  resghm  17878  mulgmhm  18434  mulgghm  18435  srglmhm  18737  srgrmhm  18738  ringlghm  18806  ringrghm  18807  gsumdixp  18811  isrhm  18925  issrngd  19065  lmodvsghm  19128  pwssplit2  19267  asclghm  19547  psrmulfval  19594  evlslem4  19716  mpfrcl  19726  xrsdsval  19998  expmhm  20023  expghm  20052  mulgghm2  20053  mulgrhm  20054  cygznlem3  20125  mamuval  20402  mamufv  20403  mvmulval  20560  mndifsplit  20653  mat2pmatmul  20749  decpmatmul  20790  fmval  21960  fmf  21962  flffval  22006  divcn  22884  rescncf  22913  htpyco1  22990  tchcph  23248  volun  23526  dyadval  23573  dvlip  23970  ftc1a  24014  ftc2ditglem  24022  tdeglem3  24033  q1pval  24127  reefgim  24418  relogoprlem  24551  eflogeq  24562  zetacvg  24955  lgsdir2  25269  lgsdchr  25294  brbtwn2  25999  ax5seglem4  26026  axeuclid  26057  axcontlem2  26059  axcontlem4  26061  axcontlem8  26065  clwwlknccat  27214  ipasslem11  28023  hhssnv  28449  mayete3i  28915  idunop  29165  idhmop  29169  0lnfn  29172  lnopmi  29187  lnophsi  29188  lnopcoi  29190  hmops  29207  hmopm  29208  nlelshi  29247  cnlnadjlem2  29255  kbass6  29308  strlem3a  29439  hstrlem3a  29447  bhmafibid1  29969  mndpluscn  30297  xrge0iifhom  30308  rezh  30340  probdsb  30809  resconn  31551  iscvm  31564  fwddifnval  32591  bj-bary1  33479  poimirlem15  33737  mbfposadd  33769  ftc1anclem3  33799  rrnmval  33938  dvhopaddN  36895  pellex  37901  rmxfval  37970  rmyfval  37971  qirropth  37974  rmxycomplete  37983  jm2.15nn0  38071  rmxdioph  38084  expdiophlem2  38090  mendvsca  38262  deg1mhm  38286  addrval  39168  subrval  39169  fmulcl  40293  fmuldfeqlem1  40294  idmgmhm  42356  resmgmhm  42366  rhmval  42487  offval0  42867
  Copyright terms: Public domain W3C validator