Theorem oveq123d 6926

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

Syntax hints:   → wi 4   = wceq 1658  (class class class)co 6905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-iota 6086  df-fv 6131  df-ov 6908

This theorem is referenced by:  csbov123  6946  prdsplusgfval  16487  prdsmulrfval  16489  prdsvscafval  16493  prdsdsval2  16497  xpsaddlem  16588  xpsvsca  16592  iscat  16685  iscatd  16686  iscatd2  16694  catcocl  16698  catass  16699  moni  16748  rcaninv  16806  subccocl  16857  isfunc  16876  funcco  16883  idfucl  16893  cofuval  16894  cofuval2  16899  cofucl  16900  funcres  16908  ressffth  16950  isnat  16959  nati  16967  fuccoval  16975  coaval  17070  catcisolem  17108  xpcco  17176  xpcco2  17180  1stfcl  17190  2ndfcl  17191  prfcl  17196  evlf2  17211  evlfcllem  17214  evlfcl  17215  curfval  17216  curf1  17218  curf12  17220  curf1cl  17221  curf2  17222  curf2val  17223  curf2cl  17224  curfcl  17225  uncfcurf  17232  hofval  17245  hof2fval  17248  hofcl  17252  yonedalem4a  17268  yonedalem3  17273  yonedainv  17274  isdlat  17546  issgrp  17638  ismndd  17666  grpsubfval  17818  grpsubpropd  17874  imasgrp  17885  subgsub  17957  eqgfval  17993  dpjfval  18808  issrg  18861  isring  18905  isringd  18939  dvrfval  19038  isdrngd  19128  issrngd  19217  islmodd  19225  isassa  19676  isassad  19684  asclfval  19695  ressascl  19705  psrval  19723  coe1tm  20003  evl1varpw  20085  isphld  20361  phlssphl  20366  pjfval  20413  islindf  20518  scmatval  20678  mdetfval  20760  smadiadetr  20850  pmatcollpw2lem  20952  pm2mpval  20970  pm2mpghm  20991  chpmatfval  21005  cpmadugsumlemB  21049  xkohmeo  21989  xpsdsval  22556  prdsxmslem2  22704  nmfval  22763  nmpropd  22768  nmpropd2  22769  subgnm  22807  tngnm  22825  cph2di  23376  cphassr  23381  ipcau2  23402  tcphcphlem2  23404  rrxplusgvscavalb  23563  q1pval  24312  r1pval  24315  dvntaylp  24524  israg  26009  ttgval  26174  grpodivfval  27944  dipfval  28112  lnoval  28162  ressnm  30196  isslmd  30300  qqhval  30563  sitgval  30939  rdgeqoa  33763  prdsbnd2  34136  isrngo  34238  lflset  35134  islfld  35137  ldualset  35200  cmtfvalN  35285  isoml  35313  ltrnfset  36192  trlfset  36235  docaffvalN  37196  diblss  37245  dihffval  37305  dihfval  37306  hvmapffval  37833  hvmapfval  37834  hgmapfval  37961  mendval  38596  hoidmvlelem3  41605  hspmbllem2  41635  isasslaw  42675  isrng  42723  lidlmsgrp  42773  lidlrng  42774  zlmodzxzscm  42982  lcoop  43047  lincvalsng  43052  lincvalpr  43054  lincdifsn  43060  islininds  43082  lines  43282