Theorem oveq123d 6106

Description: Equality deduction for operation value. (Contributed by FL, 22-Dec-2008.)

Hypotheses

Ref	Expression
oveq123d.1	|- ( ph -> F = G )
oveq123d.2	|- ( ph -> A = B )
oveq123d.3	|- ( ph -> C = D )

Assertion

Ref	Expression
oveq123d	|- ( ph -> ( A F C ) = ( B G D ) )

Proof of Theorem oveq123d

Step	Hyp	Ref	Expression
1		oveq123d.1	. . 3 |- ( ph -> F = G )
2	1	oveqd 6102	. 2 |- ( ph -> ( A F C ) = ( A G C ) )
3		oveq123d.2	. . 3 |- ( ph -> A = B )
4		oveq123d.3	. . 3 |- ( ph -> C = D )
5	3, 4	oveq12d 6103	. 2 |- ( ph -> ( A G C ) = ( B G D ) )
6	2, 5	eqtrd 2271	1 |- ( ph -> ( A F C ) = ( B G D ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  csbov123g  6124  issgrp  13718  sgrp1  13726  issgrpd  13727  ismndd  13750  grpsubfvalg  13850  grpsubpropdg  13909  imasgrp  13914  subgsub  13989  releqgg  14023  eqgex  14024  eqgfval  14025  prdsplusgfval  14184  prdsmulrfval  14186  isrng  14233  isrngd  14252  issrg  14269  srgidmlem  14282  isring  14304  ringass  14320  ringidmlem  14327  isringd  14346  ring1  14364  unitlinv  14433  unitrinv  14434  dvrfvald  14440  opprdrng  14620  islmodd  14629  islidlm  14816  rnglidlmsgrp  14834  rnglidlrng  14835  isassad  15011  asclfval  15021  ressascl  15039  psrval  15050