Theorem oveqan12d 5944

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 5934	. 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 1364  (class class class)co 5925

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  oveqan12rd  5945  offval  6147  offval3  6200  ecovdi  6714  ecovidi  6715  distrpig  7419  addcmpblnq  7453  addpipqqs  7456  mulpipq  7458  addcomnqg  7467  addcmpblnq0  7529  distrnq0  7545  recexprlem1ssl  7719  recexprlem1ssu  7720  1idsr  7854  addcnsrec  7928  mulcnsrec  7929  mulrid  8042  mulsub  8446  mulsub2  8447  muleqadd  8714  divmuldivap  8758  div2subap  8883  addltmul  9247  xnegdi  9962  fzsubel  10154  fzoval  10242  mulexp  10689  sqdivap  10714  crim  11042  readd  11053  remullem  11055  imadd  11061  cjadd  11068  cjreim  11087  sqrtmul  11219  sqabsadd  11239  sqabssub  11240  absmul  11253  abs2dif  11290  binom  11668  sinadd  11920  cosadd  11921  dvds2ln  12008  absmulgcd  12211  gcddiv  12213  bezoutr1  12227  lcmgcd  12273  nn0gcdsq  12395  crth  12419  pythagtriplem1  12461  pcqmul  12499  4sqlem4a  12587  4sqlem4  12588  prdsplusgval  12987  prdsmulrval  12989  idmhm  13173  resmhm  13191  eqgval  13431  idghm  13467  resghm  13468  isrhm  13792  rhmval  13807  xmetxp  14851  xmetxpbl  14852  txmetcnp  14862  divcnap  14909  rescncf  14925  relogoprlem  15212  lgsdir2  15382