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

Theorem oveq123d 7379
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 7375 . 2 (𝜑 → (𝐴𝐹𝐶) = (𝐴𝐺𝐶))
3 oveq123d.2 . . 3 (𝜑𝐴 = 𝐵)
4 oveq123d.3 . . 3 (𝜑𝐶 = 𝐷)
53, 4oveq12d 7376 . 2 (𝜑 → (𝐴𝐺𝐶) = (𝐵𝐺𝐷))
62, 5eqtrd 2777 1 (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = 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:  csbov123  7400  prdsplusgfval  17357  prdsmulrfval  17359  prdsvscafval  17363  prdsdsval2  17367  xpsaddlem  17456  xpsvsca  17460  iscat  17553  iscatd  17554  iscatd2  17562  catcocl  17566  catass  17567  moni  17620  rcaninv  17678  subccocl  17732  isfunc  17751  funcco  17758  idfucl  17768  cofuval  17769  cofuval2  17774  cofucl  17775  funcres  17783  ressffth  17826  isnat  17835  nati  17843  fuccoval  17853  coaval  17955  catcisolem  17997  xpcco  18072  xpcco2  18076  1stfcl  18086  2ndfcl  18087  prfcl  18092  evlf2  18108  evlfcllem  18111  evlfcl  18112  curfval  18113  curf1  18115  curf12  18117  curf1cl  18118  curf2  18119  curf2val  18120  curf2cl  18121  curfcl  18122  uncfcurf  18129  hofval  18142  hof2fval  18145  hofcl  18149  yonedalem4a  18165  yonedalem3  18170  yonedainv  18171  isdlat  18412  issgrp  18548  ismndd  18579  grpsubfval  18795  grpsubfvalALT  18796  grpsubpropd  18853  imasgrp  18864  subgsub  18941  eqgfval  18979  dpjfval  19835  issrg  19920  isring  19969  isringd  20010  dvrfval  20114  isdrngd  20215  isdrngdOLD  20217  issrngd  20323  islmodd  20331  isphld  21061  phlssphl  21066  pjfval  21115  islindf  21221  isassa  21265  isassad  21273  asclfval  21285  ressascl  21302  psrval  21320  coe1tm  21647  evl1varpw  21730  scmatval  21856  mdetfval  21938  smadiadetr  22027  pmatcollpw2lem  22129  pm2mpval  22147  pm2mpghm  22168  chpmatfval  22182  cpmadugsumlemB  22226  xkohmeo  23169  xpsdsval  23737  prdsxmslem2  23888  nmfval  23947  nmpropd  23953  nmpropd2  23954  subgnm  23992  tngnm  24018  cph2di  24574  cphassr  24579  ipcau2  24601  tcphcphlem2  24603  rrxplusgvscavalb  24762  q1pval  25521  r1pval  25524  dvntaylp  25733  israg  27642  ttgval  27820  ttgvalOLD  27821  grpodivfval  29479  dipfval  29647  lnoval  29697  ressnm  31821  isslmd  32040  idlinsubrg  32208  fedgmullem2  32328  qqhval  32558  sitgval  32935  rdgeqoa  35844  prdsbnd2  36257  isrngo  36359  lflset  37524  islfld  37527  ldualset  37590  cmtfvalN  37675  isoml  37703  ltrnfset  38583  trlfset  38626  docaffvalN  39587  diblss  39636  dihffval  39696  dihfval  39697  hvmapffval  40224  hvmapfval  40225  hgmapfval  40352  imacrhmcl  40698  mendval  41513  hoidmvlelem3  44845  hspmbllem2  44875  isasslaw  46133  isrng  46181  lidlmsgrp  46231  lidlrng  46232  zlmodzxzscm  46440  lcoop  46499  lincvalsng  46504  lincvalpr  46506  lincdifsn  46512  islininds  46534  lines  46824  mndtchom  47117  mndtcco  47118  mndtccatid  47120
  Copyright terms: Public domain W3C validator