Theorem oveqan12d 5869

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 5859	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	syl2an 287	1 |- ( ( ph /\ ps ) -> ( A F C ) = ( B F D ) )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1348  (class class class)co 5850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204  df-ov 5853

This theorem is referenced by:  oveqan12rd  5870  offval  6065  offval3  6110  ecovdi  6620  ecovidi  6621  distrpig  7282  addcmpblnq  7316  addpipqqs  7319  mulpipq  7321  addcomnqg  7330  addcmpblnq0  7392  distrnq0  7408  recexprlem1ssl  7582  recexprlem1ssu  7583  1idsr  7717  addcnsrec  7791  mulcnsrec  7792  mulid1  7904  mulsub  8307  mulsub2  8308  muleqadd  8573  divmuldivap  8616  div2subap  8741  addltmul  9101  xnegdi  9812  fzsubel  10003  fzoval  10091  mulexp  10502  sqdivap  10527  crim  10809  readd  10820  remullem  10822  imadd  10828  cjadd  10835  cjreim  10854  sqrtmul  10986  sqabsadd  11006  sqabssub  11007  absmul  11020  abs2dif  11057  binom  11434  sinadd  11686  cosadd  11687  dvds2ln  11773  absmulgcd  11959  gcddiv  11961  bezoutr1  11975  lcmgcd  12019  nn0gcdsq  12141  crth  12165  pythagtriplem1  12206  pcqmul  12244  4sqlem4a  12330  4sqlem4  12331  idmhm  12678  xmetxp  13222  xmetxpbl  13223  txmetcnp  13233  divcnap  13270  rescncf  13283  relogoprlem  13504  lgsdir2  13649