Theorem oveq123d 7441

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

Step	Hyp	Ref	Expression
1		oveq123d.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2	1	oveqd 7437	. 2 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐴𝐺𝐶))
3		oveq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4		oveq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	oveq12d 7438	. 2 ⊢ (𝜑 → (𝐴𝐺𝐶) = (𝐵𝐺𝐷))
6	2, 5	eqtrd 2796	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  csbov123  7464  prdsplusgfval  17645  prdsmulrfval  17647  prdsvscafval  17651  prdsdsval2  17655  xpsaddlem  17745  xpsvsca  17749  iscat  17846  iscatd  17847  iscatd2  17855  catcocl  17859  catass  17860  moni  17911  rcaninv  17969  subccocl  18020  isfunc  18039  funcco  18046  idfucl  18056  cofuval  18057  cofuval2  18062  cofucl  18063  funcres  18071  ressffth  18115  isnat  18125  nati  18133  fuccoval  18141  coaval  18243  catcisolem  18285  xpcco  18357  xpcco2  18361  1stfcl  18371  2ndfcl  18372  prfcl  18377  evlf2  18392  evlfcllem  18395  evlfcl  18396  curfval  18397  curf1  18399  curf12  18401  curf1cl  18402  curf2  18403  curf2val  18404  curf2cl  18405  curfcl  18406  uncfcurf  18413  hofval  18426  hof2fval  18429  hofcl  18433  yonedalem4a  18449  yonedalem3  18454  yonedainv  18455  isdlat  18696  issgrp  18909  issgrpd  18919  ismndd  18946  grpsubfval  19194  grpsubfvalALT  19195  grpsubpropd  19255  imasgrp  19266  subgsub  19349  eqgfval  19388  dpjfval  20271  isrng  20376  isrngd  20395  issrg  20414  isring  20463  isringd  20522  dvrfval  20632  isdrngd  21022  isdrngdOLD  21024  issrngd  21112  islmodd  21141  rnglidlmsgrp  21534  rnglidlrng  21535  rngqiprngimf1lem  21590  isphld  21960  phlssphl  21965  pjfval  22012  islindf  22118  isassa  22164  isassad  22173  asclfval  22186  ressascl  22204  psrval  22223  psdffval  22478  coe1tm  22592  evl1varpw  22679  evls1maplmhm  22695  scmatval  22819  mdetfval  22901  smadiadetr  22990  pmatcollpw2lem  23095  pm2mpval  23113  pm2mpghm  23134  chpmatfval  23148  cpmadugsumlemB  23192  xkohmeo  24134  xpsdsval  24700  prdsxmslem2  24848  nmfval  24907  nmpropd  24913  nmpropd2  24914  subgnm  24952  tngnm  24970  cph2di  25528  cphassr  25533  ipcau2  25555  tcphcphlem2  25557  rrxplusgvscavalb  25716  q1pval  26473  r1pval  26476  dvntaylp  26698  israg  29172  ttgval  29452  grpodivfval  31136  dipfval  31304  lnoval  31354  ressnm  33525  isslmd  33763  erlval  33819  rlocval  33820  idlinsubrg  33981  zringfrac  34086  vietalem  34211  fedgmullem2  34262  qqhval  34604  sitgval  34964  rdgeqoa  38293  prdsbnd2  38729  isrngo  38831  lflset  40116  islfld  40119  ldualset  40182  cmtfvalN  40267  isoml  40295  ltrnfset  41174  trlfset  41217  docaffvalN  42178  diblss  42227  dihffval  42287  dihfval  42288  hvmapffval  42815  hvmapfval  42816  hgmapfval  42943  isprimroot  43143  primrootsunit1  43147  aks6d1c1p4  43161  aks5lem3a  43239  imacrhmcl  43581  prjspnnorm  43661  mendval  44180  hoidmvlelem3  47606  hspmbllem2  47636  isasslaw  49288  zlmodzxzscm  49468  lcoop  49522  lincvalsng  49527  lincvalpr  49529  lincdifsn  49535  islininds  49557  lines  49842  discsubc  50171  cofu2a  50202  cofid2  50222  cofidf2  50227  imaf1co  50262  upciclem1  50273  upfval2  50284  upfval3  50285  isuplem  50286  oppcup3lem  50313  uptrlem1  50317  uptr2  50328  swapfcoa  50388  tposcurf2val  50408  fuco21  50443  fuco23  50448  fuco22natlem3  50451  fucoid  50455  fucocolem2  50461  fucocolem4  50463  oppfdiag  50523  oppcthinendcALT  50548  isinito2lem  50605  dfinito4  50608  mndtchom  50691  mndtcco  50692  mndtccatid  50694  2arwcat  50707  setc1onsubc  50709  lanfval  50720  ranfval  50721  lanpropd  50722  ranpropd  50723  lanup  50748  ranup  50749  lmdfval  50756  cmdfval  50757  lmdpropd  50764  cmdpropd  50765  concom  50770  coccom  50771  islmd  50772  iscmd  50773  cmddu  50775