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

Theorem oveqan12d 7303
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 7293 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3syl2an 596 1 ((𝜑𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1539  (class class class)co 7284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287
This theorem is referenced by:  oveqan12rd  7304  offval  7551  offval3  7834  odi  8419  omopth2  8424  oeoa  8437  ecovdi  8623  ackbij1lem9  9993  distrpi  10663  addpipq  10702  mulpipq  10705  lterpq  10735  reclem3pr  10814  1idsr  10863  mulcnsr  10901  mulid1  10982  1re  10984  mul02  11162  addcom  11170  mulsub  11427  mulsub2  11428  muleqadd  11628  divmuldiv  11684  div2sub  11809  addltmul  12218  xnegdi  12991  xadddilem  13037  fzsubel  13301  fzoval  13397  seqid3  13776  mulexp  13831  sqdiv  13850  hashdom  14103  hashun  14106  ccatfval  14285  splcl  14474  crim  14835  readd  14846  remullem  14848  imadd  14854  cjadd  14861  cjreim  14880  sqrtmul  14980  sqabsadd  15003  sqabssub  15004  absmul  15015  abs2dif  15053  bhmafibid1  15186  binom  15551  binomfallfac  15760  sinadd  15882  cosadd  15883  dvds2ln  16007  sadcaddlem  16173  bezoutlem4  16259  bezout  16260  absmulgcd  16266  gcddiv  16268  bezoutr1  16283  lcmgcd  16321  lcmfass  16360  nn0gcdsq  16465  crth  16488  pythagtriplem1  16526  pcqmul  16563  4sqlem4a  16661  4sqlem4  16662  prdsplusgval  17193  prdsmulrval  17195  prdsdsval  17198  prdsvscaval  17199  idmhm  18448  0mhm  18467  resmhm  18468  prdspjmhm  18476  pwsdiagmhm  18478  gsumws2  18490  frmdup1  18512  eqgval  18814  idghm  18858  resghm  18859  mulgmhm  19438  mulgghm  19439  srglmhm  19780  srgrmhm  19781  ringlghm  19852  ringrghm  19853  gsumdixp  19857  isrhm  19974  issrngd  20130  lmodvsghm  20193  pwssplit2  20331  xrsdsval  20651  expmhm  20676  expghm  20706  mulgghm2  20707  mulgrhm  20708  cygznlem3  20786  asclghm  21096  psrmulfval  21163  evlslem4  21293  mpfrcl  21304  mamuval  21544  mamufv  21545  mvmulval  21701  mndifsplit  21794  mat2pmatmul  21889  decpmatmul  21930  fmval  23103  fmf  23105  flffval  23149  divcn  24040  rescncf  24069  htpyco1  24150  tcphcph  24410  rrxdsfival  24586  ehl2eudisval  24596  volun  24718  dyadval  24765  dvlip  25166  ftc1a  25210  ftc2ditglem  25218  tdeglem3  25231  tdeglem3OLD  25232  q1pval  25327  reefgim  25618  relogoprlem  25755  eflogeq  25766  zetacvg  26173  lgsdir2  26487  lgsdchr  26512  2sq2  26590  2sqnn0  26595  brbtwn2  27282  ax5seglem4  27309  axeuclid  27340  axcontlem2  27342  axcontlem4  27344  axcontlem8  27348  clwwlknccat  28436  ex-fpar  28835  ipasslem11  29211  hhssnv  29635  mayete3i  30099  idunop  30349  idhmop  30353  0lnfn  30356  lnopmi  30371  lnophsi  30372  lnopcoi  30374  hmops  30391  hmopm  30392  nlelshi  30431  cnlnadjlem2  30439  kbass6  30492  strlem3a  30623  hstrlem3a  30631  mndpluscn  31885  xrge0iifhom  31896  rezh  31930  probdsb  32398  resconn  33217  iscvm  33230  satfdmlem  33339  satffunlem1lem1  33373  satffunlem2lem1  33375  fwddifnval  34474  bj-bary1  35492  poimirlem15  35801  mbfposadd  35833  ftc1anclem3  35861  rrnmval  35995  dvhopaddN  39135  nnadddir  40307  cnreeu  40445  prjcrvfval  40475  pellex  40664  rmxfval  40733  rmyfval  40734  qirropth  40737  rmxycomplete  40746  jm2.15nn0  40832  rmxdioph  40845  expdiophlem2  40851  mendvsca  41023  deg1mhm  41039  mnringmulrvald  41852  addrval  42091  subrval  42092  fmulcl  43129  fmuldfeqlem1  43130  idmgmhm  45353  resmgmhm  45363  rhmval  45488  line  46089  itsclc0xyqsolr  46126
  Copyright terms: Public domain W3C validator