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

Theorem oveqan12d 7377
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 7367 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3syl2an 597 1 ((𝜑𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  (class class class)co 7358
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  oveqan12rd  7378  offval  7627  offval3  7916  odi  8527  omopth2  8532  oeoa  8545  ecovdi  8765  ackbij1lem9  10165  distrpi  10835  addpipq  10874  mulpipq  10877  lterpq  10907  reclem3pr  10986  1idsr  11035  mulcnsr  11073  mulid1  11154  1re  11156  mul02  11334  addcom  11342  mulsub  11599  mulsub2  11600  muleqadd  11800  divmuldiv  11856  div2sub  11981  addltmul  12390  xnegdi  13168  xadddilem  13214  fzsubel  13478  fzoval  13574  seqid3  13953  mulexp  14008  sqdiv  14027  hashdom  14280  hashun  14283  ccatfval  14462  splcl  14641  crim  15001  readd  15012  remullem  15014  imadd  15020  cjadd  15027  cjreim  15046  sqrtmul  15145  sqabsadd  15168  sqabssub  15169  absmul  15180  abs2dif  15218  bhmafibid1  15351  binom  15716  binomfallfac  15925  sinadd  16047  cosadd  16048  dvds2ln  16172  sadcaddlem  16338  bezoutlem4  16424  bezout  16425  absmulgcd  16431  gcddiv  16433  bezoutr1  16446  lcmgcd  16484  lcmfass  16523  nn0gcdsq  16628  crth  16651  pythagtriplem1  16689  pcqmul  16726  4sqlem4a  16824  4sqlem4  16825  prdsplusgval  17356  prdsmulrval  17358  prdsdsval  17361  prdsvscaval  17362  idmhm  18612  0mhm  18631  resmhm  18632  prdspjmhm  18640  pwsdiagmhm  18642  gsumws2  18653  frmdup1  18675  eqgval  18980  idghm  19024  resghm  19025  mulgmhm  19607  mulgghm  19608  srglmhm  19953  srgrmhm  19954  ringlghm  20029  ringrghm  20030  gsumdixp  20034  isrhm  20153  issrngd  20323  lmodvsghm  20386  pwssplit2  20524  xrsdsval  20844  expmhm  20869  expghm  20899  mulgghm2  20900  mulgrhm  20901  cygznlem3  20979  asclghm  21289  psrmulfval  21356  evlslem4  21487  mpfrcl  21498  mamuval  21738  mamufv  21739  mvmulval  21895  mndifsplit  21988  mat2pmatmul  22083  decpmatmul  22124  fmval  23297  fmf  23299  flffval  23343  divcn  24234  rescncf  24263  htpyco1  24344  tcphcph  24604  rrxdsfival  24780  ehl2eudisval  24790  volun  24912  dyadval  24959  dvlip  25360  ftc1a  25404  ftc2ditglem  25412  tdeglem3  25425  tdeglem3OLD  25426  q1pval  25521  reefgim  25812  relogoprlem  25949  eflogeq  25960  zetacvg  26367  lgsdir2  26681  lgsdchr  26706  2sq2  26784  2sqnn0  26789  negsdi  27349  brbtwn2  27857  ax5seglem4  27884  axeuclid  27915  axcontlem2  27917  axcontlem4  27919  axcontlem8  27923  clwwlknccat  29010  ex-fpar  29409  ipasslem11  29785  hhssnv  30209  mayete3i  30673  idunop  30923  idhmop  30927  0lnfn  30930  lnopmi  30945  lnophsi  30946  lnopcoi  30948  hmops  30965  hmopm  30966  nlelshi  31005  cnlnadjlem2  31013  kbass6  31066  strlem3a  31197  hstrlem3a  31205  mndpluscn  32510  xrge0iifhom  32521  rezh  32555  probdsb  33025  resconn  33843  iscvm  33856  satfdmlem  33965  satffunlem1lem1  33999  satffunlem2lem1  34001  fwddifnval  34751  bj-bary1  35786  poimirlem15  36096  mbfposadd  36128  ftc1anclem3  36156  rrnmval  36290  dvhopaddN  39580  nnadddir  40789  cnreeu  40940  prjcrvfval  40972  pellex  41161  rmxfval  41230  rmyfval  41231  qirropth  41234  rmxycomplete  41244  jm2.15nn0  41330  rmxdioph  41343  expdiophlem2  41349  mendvsca  41521  deg1mhm  41537  mnringmulrvald  42514  addrval  42753  subrval  42754  fmulcl  43829  fmuldfeqlem1  43830  idmgmhm  46089  resmgmhm  46099  rhmval  46224  line  46825  itsclc0xyqsolr  46862
  Copyright terms: Public domain W3C validator