Theorem oveqan12d 5938

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 5928	. 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 5919

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922

This theorem is referenced by:  oveqan12rd  5939  offval  6140  offval3  6188  ecovdi  6702  ecovidi  6703  distrpig  7395  addcmpblnq  7429  addpipqqs  7432  mulpipq  7434  addcomnqg  7443  addcmpblnq0  7505  distrnq0  7521  recexprlem1ssl  7695  recexprlem1ssu  7696  1idsr  7830  addcnsrec  7904  mulcnsrec  7905  mulrid  8018  mulsub  8422  mulsub2  8423  muleqadd  8689  divmuldivap  8733  div2subap  8858  addltmul  9222  xnegdi  9937  fzsubel  10129  fzoval  10217  mulexp  10652  sqdivap  10677  crim  11005  readd  11016  remullem  11018  imadd  11024  cjadd  11031  cjreim  11050  sqrtmul  11182  sqabsadd  11202  sqabssub  11203  absmul  11216  abs2dif  11253  binom  11630  sinadd  11882  cosadd  11883  dvds2ln  11970  absmulgcd  12157  gcddiv  12159  bezoutr1  12173  lcmgcd  12219  nn0gcdsq  12341  crth  12365  pythagtriplem1  12406  pcqmul  12444  4sqlem4a  12532  4sqlem4  12533  idmhm  13044  resmhm  13062  eqgval  13296  idghm  13332  resghm  13333  isrhm  13657  rhmval  13672  xmetxp  14686  xmetxpbl  14687  txmetcnp  14697  divcnap  14744  rescncf  14760  relogoprlem  15044  lgsdir2  15190