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

Theorem oveq123d 7172
Description: Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)
Hypotheses
Ref Expression
oveq123d.1 (𝜑𝐹 = 𝐺)
oveq123d.2 (𝜑𝐴 = 𝐵)
oveq123d.3 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
oveq123d (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))

Proof of Theorem oveq123d
StepHypRef Expression
1 oveq123d.1 . . 3 (𝜑𝐹 = 𝐺)
21oveqd 7168 . 2 (𝜑 → (𝐴𝐹𝐶) = (𝐴𝐺𝐶))
3 oveq123d.2 . . 3 (𝜑𝐴 = 𝐵)
4 oveq123d.3 . . 3 (𝜑𝐶 = 𝐷)
53, 4oveq12d 7169 . 2 (𝜑 → (𝐴𝐺𝐶) = (𝐵𝐺𝐷))
62, 5eqtrd 2860 1 (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  (class class class)co 7151
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-rex 3148  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4837  df-br 5063  df-iota 6311  df-fv 6359  df-ov 7154
This theorem is referenced by:  csbov123  7193  prdsplusgfval  16739  prdsmulrfval  16741  prdsvscafval  16745  prdsdsval2  16749  xpsaddlem  16838  xpsvsca  16842  iscat  16935  iscatd  16936  iscatd2  16944  catcocl  16948  catass  16949  moni  16998  rcaninv  17056  subccocl  17107  isfunc  17126  funcco  17133  idfucl  17143  cofuval  17144  cofuval2  17149  cofucl  17150  funcres  17158  ressffth  17200  isnat  17209  nati  17217  fuccoval  17225  coaval  17320  catcisolem  17358  xpcco  17425  xpcco2  17429  1stfcl  17439  2ndfcl  17440  prfcl  17445  evlf2  17460  evlfcllem  17463  evlfcl  17464  curfval  17465  curf1  17467  curf12  17469  curf1cl  17470  curf2  17471  curf2val  17472  curf2cl  17473  curfcl  17474  uncfcurf  17481  hofval  17494  hof2fval  17497  hofcl  17501  yonedalem4a  17517  yonedalem3  17522  yonedainv  17523  isdlat  17795  issgrp  17893  ismndd  17923  grpsubfval  18079  grpsubfvalALT  18080  grpsubpropd  18136  imasgrp  18147  subgsub  18223  eqgfval  18260  dpjfval  19099  issrg  19179  isring  19223  isringd  19257  dvrfval  19356  isdrngd  19449  issrngd  19554  islmodd  19562  isassa  20009  isassad  20017  asclfval  20029  ressascl  20046  psrval  20063  coe1tm  20358  evl1varpw  20440  isphld  20714  phlssphl  20719  pjfval  20766  islindf  20872  scmatval  21029  mdetfval  21111  smadiadetr  21200  pmatcollpw2lem  21301  pm2mpval  21319  pm2mpghm  21340  chpmatfval  21354  cpmadugsumlemB  21398  xkohmeo  22339  xpsdsval  22906  prdsxmslem2  23054  nmfval  23113  nmpropd  23118  nmpropd2  23119  subgnm  23157  tngnm  23175  cph2di  23726  cphassr  23731  ipcau2  23752  tcphcphlem2  23754  rrxplusgvscavalb  23913  q1pval  24662  r1pval  24665  dvntaylp  24874  israg  26397  ttgval  26576  grpodivfval  28226  dipfval  28394  lnoval  28444  ressnm  30553  isslmd  30745  fedgmullem2  30913  qqhval  31102  sitgval  31477  rdgeqoa  34521  prdsbnd2  34942  isrngo  35044  lflset  36063  islfld  36066  ldualset  36129  cmtfvalN  36214  isoml  36242  ltrnfset  37121  trlfset  37164  docaffvalN  38125  diblss  38174  dihffval  38234  dihfval  38235  hvmapffval  38762  hvmapfval  38763  hgmapfval  38890  mendval  39645  hoidmvlelem3  42742  hspmbllem2  42772  isasslaw  43928  isrng  43976  lidlmsgrp  44026  lidlrng  44027  zlmodzxzscm  44234  lcoop  44295  lincvalsng  44300  lincvalpr  44302  lincdifsn  44308  islininds  44330  lines  44547
  Copyright terms: Public domain W3C validator