Theorem oveq123d 6570

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

Syntax hints:   → wi 4   = wceq 1475  (class class class)co 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  csbov123  6585  prdsplusgfval  15957  prdsmulrfval  15959  prdsvscafval  15963  prdsdsval2  15967  xpsaddlem  16058  xpsvsca  16062  iscat  16156  iscatd  16157  iscatd2  16165  catcocl  16169  catass  16170  moni  16219  rcaninv  16277  subccocl  16328  isfunc  16347  funcco  16354  idfucl  16364  cofuval  16365  cofuval2  16370  cofucl  16371  funcres  16379  ressffth  16421  isnat  16430  nati  16438  fuccoval  16446  coaval  16541  catcisolem  16579  xpcco  16646  xpcco2  16650  1stfcl  16660  2ndfcl  16661  prfcl  16666  evlf2  16681  evlfcllem  16684  evlfcl  16685  curfval  16686  curf1  16688  curf12  16690  curf1cl  16691  curf2  16692  curf2val  16693  curf2cl  16694  curfcl  16695  uncfcurf  16702  hofval  16715  hof2fval  16718  hofcl  16722  yonedalem4a  16738  yonedalem3  16743  yonedainv  16744  isdlat  17016  issgrp  17108  ismndd  17136  grpsubfval  17287  grpsubpropd  17343  imasgrp  17354  subgsub  17429  eqgfval  17465  dpjfval  18277  issrg  18330  isring  18374  isringd  18408  dvrfval  18507  isdrngd  18595  issrngd  18684  islmodd  18692  isassa  19136  isassad  19144  asclfval  19155  ressascl  19165  psrval  19183  coe1tm  19464  evl1varpw  19546  isphld  19818  pjfval  19869  islindf  19970  scmatval  20129  mdetfval  20211  smadiadetr  20300  pmatcollpw2lem  20401  pm2mpval  20419  pm2mpghm  20440  chpmatfval  20454  cpmadugsumlemB  20498  xkohmeo  21428  xpsdsval  21996  prdsxmslem2  22144  nmfval  22203  nmpropd  22208  nmpropd2  22209  subgnm  22247  tngnm  22265  cph2di  22815  cphassr  22820  ipcau2  22841  tchcphlem2  22843  q1pval  23717  r1pval  23720  dvntaylp  23929  israg  25392  ttgval  25555  grpodivfval  26772  dipfval  26941  lnoval  26991  ressnm  28982  isslmd  29086  qqhval  29346  sitgval  29721  rdgeqoa  32394  prdsbnd2  32764  isrngo  32866  lflset  33364  islfld  33367  ldualset  33430  cmtfvalN  33515  isoml  33543  ltrnfset  34421  trlfset  34465  docaffvalN  35428  diblss  35477  dihffval  35537  dihfval  35538  hvmapffval  36065  hvmapfval  36066  hgmapfval  36196  mendval  36772  hoidmvlelem3  39487  hspmbllem2  39517  isasslaw  41618  isrng  41666  lidlmsgrp  41716  lidlrng  41717  zlmodzxzscm  41928  lcoop  41994  lincvalsng  41999  lincvalpr  42001  lincdifsn  42007  islininds  42029