Theorem oveq123d 7445

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427

This theorem is used by:  csbov123  7468  prdsplusgfval  17654  prdsmulrfval  17656  prdsvscafval  17660  prdsdsval2  17664  xpsaddlem  17754  xpsvsca  17758  iscat  17855  iscatd  17856  iscatd2  17864  catcocl  17868  catass  17869  moni  17920  rcaninv  17978  subccocl  18029  isfunc  18048  funcco  18055  idfucl  18065  cofuval  18066  cofuval2  18071  cofucl  18072  funcres  18080  ressffth  18124  isnat  18134  nati  18142  fuccoval  18150  coaval  18252  catcisolem  18294  xpcco  18366  xpcco2  18370  1stfcl  18380  2ndfcl  18381  prfcl  18386  evlf2  18401  evlfcllem  18404  evlfcl  18405  curfval  18406  curf1  18408  curf12  18410  curf1cl  18411  curf2  18412  curf2val  18413  curf2cl  18414  curfcl  18415  uncfcurf  18422  hofval  18435  hof2fval  18438  hofcl  18442  yonedalem4a  18458  yonedalem3  18463  yonedainv  18464  isdlat  18705  issgrp  18918  issgrpd  18928  ismndd  18955  grpsubfval  19203  grpsubfvalALT  19204  grpsubpropd  19264  imasgrp  19275  subgsub  19358  eqgfval  19397  dpjfval  20280  isrng  20385  isrngd  20404  issrg  20423  isring  20472  isringd  20531  dvrfval  20641  isdrngd  21031  isdrngdOLD  21033  issrngd  21121  islmodd  21150  rnglidlmsgrp  21543  rnglidlrng  21544  rngqiprngimf1lem  21599  isphld  21969  phlssphl  21974  pjfval  22021  islindf  22127  isassa  22173  isassad  22182  asclfval  22195  ressascl  22213  psrval  22232  psdffval  22487  coe1tm  22601  evl1varpw  22688  evls1maplmhm  22704  scmatval  22828  mdetfval  22910  smadiadetr  22999  pmatcollpw2lem  23104  pm2mpval  23122  pm2mpghm  23143  chpmatfval  23157  cpmadugsumlemB  23201  xkohmeo  24143  xpsdsval  24709  prdsxmslem2  24857  nmfval  24916  nmpropd  24922  nmpropd2  24923  subgnm  24961  tngnm  24979  cph2di  25537  cphassr  25542  ipcau2  25564  tcphcphlem2  25566  rrxplusgvscavalb  25725  q1pval  26482  r1pval  26485  dvntaylp  26707  israg  29181  ttgval  29461  grpodivfval  31145  dipfval  31313  lnoval  31363  ressnm  33575  isslmd  33813  erlval  33869  rlocval  33870  idlinsubrg  34031  zringfrac  34136  vietalem  34261  fedgmullem2  34312  qqhval  34654  sitgval  35014  rdgeqoa  38430  prdsbnd2  38866  isrngo  38968  lflset  40253  islfld  40256  ldualset  40319  cmtfvalN  40404  isoml  40432  ltrnfset  41311  trlfset  41354  docaffvalN  42315  diblss  42364  dihffval  42424  dihfval  42425  hvmapffval  42952  hvmapfval  42953  hgmapfval  43080  isprimroot  43280  primrootsunit1  43284  aks6d1c1p4  43298  aks5lem3a  43376  imacrhmcl  43718  prjspnnorm  43798  mendval  44318  hoidmvlelem3  47743  hspmbllem2  47773  isasslaw  49425  zlmodzxzscm  49605  lcoop  49659  lincvalsng  49664  lincvalpr  49666  lincdifsn  49672  islininds  49694  lines  49980  discsubc  50314  cofu2a  50346  cofid2  50367  cofidf2  50372  imaf1co  50407  upciclem1  50418  upfval2  50429  upfval3  50430  isuplem  50431  oppcup3lem  50458  uptrlem1  50462  uptr2  50473  swapfcoa  50539  tposcurf2val  50559  fuco21  50594  fuco23  50599  fuco22natlem3  50602  fucoid  50606  fucocolem2  50612  fucocolem4  50614  oppfdiag  50687  oppcthinendcALT  50712  isinito2lem  50769  dfinito4  50772  mndtchom  50858  mndtcco  50859  mndtccatid  50861  2arwcat  50874  setc1onsubc  50876  parcoval2  50902  parmapfunc2  50910  parmapfunc  50911  lanfval  50932  ranfval  50933  lanpropd  50934  ranpropd  50935  lanup  50960  ranup  50961  lmdfval  50968  cmdfval  50969  lmdpropd  50976  cmdpropd  50977  concom  50982  coccom  50983  islmd  50984  iscmd  50985  cmddu  50987