Theorem oveq123d 7435

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 7431	. 2 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐴𝐺𝐶))
3		oveq123d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4		oveq123d.3	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	oveq12d 7432	. 2 ⊢ (𝜑 → (𝐴𝐺𝐶) = (𝐵𝐺𝐷))
6	2, 5	eqtrd 2795	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐺𝐷))

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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 6489  df-fv 6541  df-ov 7417

This theorem is used by:  csbov123  7458  prdsplusgfval  17560  prdsmulrfval  17562  prdsvscafval  17566  prdsdsval2  17570  xpsaddlem  17660  xpsvsca  17664  iscat  17761  iscatd  17762  iscatd2  17770  catcocl  17774  catass  17775  moni  17826  rcaninv  17884  subccocl  17935  isfunc  17954  funcco  17961  idfucl  17971  cofuval  17972  cofuval2  17977  cofucl  17978  funcres  17986  ressffth  18030  isnat  18040  nati  18048  fuccoval  18056  coaval  18158  catcisolem  18200  xpcco  18272  xpcco2  18276  1stfcl  18286  2ndfcl  18287  prfcl  18292  evlf2  18307  evlfcllem  18310  evlfcl  18311  curfval  18312  curf1  18314  curf12  18316  curf1cl  18317  curf2  18318  curf2val  18319  curf2cl  18320  curfcl  18321  uncfcurf  18328  hofval  18341  hof2fval  18344  hofcl  18348  yonedalem4a  18364  yonedalem3  18369  yonedainv  18370  isdlat  18611  issgrp  18823  issgrpd  18833  ismndd  18860  grpsubfval  19108  grpsubfvalALT  19109  grpsubpropd  19169  imasgrp  19180  subgsub  19263  eqgfval  19302  dpjfval  20185  isrng  20290  isrngd  20309  issrg  20328  isring  20377  isringd  20434  dvrfval  20544  isdrngd  20932  isdrngdOLD  20934  issrngd  21022  islmodd  21051  rnglidlmsgrp  21444  rnglidlrng  21445  rngqiprngimf1lem  21498  isphld  21868  phlssphl  21873  pjfval  21920  islindf  22026  isassa  22072  isassad  22081  asclfval  22094  ressascl  22112  psrval  22131  psdffval  22386  coe1tm  22500  evl1varpw  22587  evls1maplmhm  22603  scmatval  22727  mdetfval  22809  smadiadetr  22898  pmatcollpw2lem  23003  pm2mpval  23021  pm2mpghm  23042  chpmatfval  23056  cpmadugsumlemB  23100  xkohmeo  24042  xpsdsval  24608  prdsxmslem2  24756  nmfval  24815  nmpropd  24821  nmpropd2  24822  subgnm  24860  tngnm  24878  cph2di  25436  cphassr  25441  ipcau2  25463  tcphcphlem2  25465  rrxplusgvscavalb  25624  q1pval  26381  r1pval  26384  dvntaylp  26608  israg  29052  ttgval  29332  grpodivfval  31016  dipfval  31184  lnoval  31234  ressnm  33405  isslmd  33643  erlval  33699  rlocval  33700  idlinsubrg  33860  zringfrac  33965  vietalem  34090  fedgmullem2  34141  qqhval  34483  sitgval  34844  rdgeqoa  38125  prdsbnd2  38546  isrngo  38648  lflset  39933  islfld  39936  ldualset  39999  cmtfvalN  40084  isoml  40112  ltrnfset  40991  trlfset  41034  docaffvalN  41995  diblss  42044  dihffval  42104  dihfval  42105  hvmapffval  42632  hvmapfval  42633  hgmapfval  42760  isprimroot  42960  primrootsunit1  42964  aks6d1c1p4  42978  aks5lem3a  43056  imacrhmcl  43403  mendval  44021  hoidmvlelem3  47426  hspmbllem2  47456  isasslaw  49108  zlmodzxzscm  49288  lcoop  49342  lincvalsng  49347  lincvalpr  49349  lincdifsn  49355  islininds  49377  lines  49662  discsubc  49991  cofu2a  50022  cofid2  50042  cofidf2  50047  imaf1co  50082  upciclem1  50093  upfval2  50104  upfval3  50105  isuplem  50106  oppcup3lem  50133  uptrlem1  50137  uptr2  50148  swapfcoa  50208  tposcurf2val  50228  fuco21  50263  fuco23  50268  fuco22natlem3  50271  fucoid  50275  fucocolem2  50281  fucocolem4  50283  oppfdiag  50343  oppcthinendcALT  50368  isinito2lem  50425  dfinito4  50428  mndtchom  50511  mndtcco  50512  mndtccatid  50514  2arwcat  50527  setc1onsubc  50529  lanfval  50540  ranfval  50541  lanpropd  50542  ranpropd  50543  lanup  50568  ranup  50569  lmdfval  50576  cmdfval  50577  lmdpropd  50584  cmdpropd  50585  concom  50590  coccom  50591  islmd  50592  iscmd  50593  cmddu  50595