Theorem oveqan12d 6032

Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)

Hypotheses

Ref	Expression
oveq1d.1	|- ( ph -> A = B )
opreqan12i.2	|- ( ps -> C = D )

Assertion

Ref	Expression
oveqan12d	|- ( ( ph /\ ps ) -> ( A F C ) = ( B F D ) )

Proof of Theorem oveqan12d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		opreqan12i.2	. 2 |- ( ps -> C = D )
3		oveq12 6022	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	syl2an 289	1 |- ( ( ph /\ ps ) -> ( A F C ) = ( B F D ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1395  (class class class)co 6013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  oveqan12rd  6033  offval  6238  offval3  6291  ecovdi  6810  ecovidi  6811  distrpig  7543  addcmpblnq  7577  addpipqqs  7580  mulpipq  7582  addcomnqg  7591  addcmpblnq0  7653  distrnq0  7669  recexprlem1ssl  7843  recexprlem1ssu  7844  1idsr  7978  addcnsrec  8052  mulcnsrec  8053  mulrid  8166  mulsub  8570  mulsub2  8571  muleqadd  8838  divmuldivap  8882  div2subap  9007  addltmul  9371  xnegdi  10093  fzsubel  10285  fzoval  10373  mulexp  10830  sqdivap  10855  crim  11409  readd  11420  remullem  11422  imadd  11428  cjadd  11435  cjreim  11454  sqrtmul  11586  sqabsadd  11606  sqabssub  11607  absmul  11620  abs2dif  11657  binom  12035  sinadd  12287  cosadd  12288  dvds2ln  12375  absmulgcd  12578  gcddiv  12580  bezoutr1  12594  lcmgcd  12640  nn0gcdsq  12762  crth  12786  pythagtriplem1  12828  pcqmul  12866  4sqlem4a  12954  4sqlem4  12955  prdsplusgval  13356  prdsmulrval  13358  idmhm  13542  resmhm  13560  eqgval  13800  idghm  13836  resghm  13837  isrhm  14162  rhmval  14177  xmetxp  15221  xmetxpbl  15222  txmetcnp  15232  divcnap  15279  rescncf  15295  relogoprlem  15582  lgsdir2  15752  clwwlknccat  16218