Theorem oveq12d 5530

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Hypotheses

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

Assertion

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

Proof of Theorem oveq12d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		oveq12d.2	. 2 |- ( ph -> C = D )
3		oveq12 5521	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	syl2anc 391	1 |- ( ph -> ( A F C ) = ( B F D ) )

Syntax hints:   -> wi 4   = wceq 1243  (class class class)co 5512

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515

This theorem is referenced by:  oveq123d  5533  ovmpt2dxf  5626  ovmpt2df  5632  caovdig  5675  caovdir2d  5677  caovdirg  5678  caovdilemd  5692  caovlem2d  5693  offval  5719  fnofval  5721  offval2  5726  ofco  5729  caofinvl  5733  offres  5762  nnmsucr  6067  nndir  6069  ecovdi  6217  ecovidi  6218  dfplpq2  6452  dfmpq2  6453  addcmpblnq  6465  mulpipqqs  6471  addassnqg  6480  distrnqg  6485  ltaddnq  6505  halfnqq  6508  enq0tr  6532  addcmpblnq0  6541  addnq0mo  6545  addnnnq0  6547  nqnq0a  6552  distrnq0  6557  addassnq0  6560  distnq0r  6561  nq02m  6563  ltexpri  6711  cauappcvgprlemm  6743  cauappcvgprlemloc  6750  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  cauappcvgprlem2  6758  cauappcvgprlemlim  6759  cauappcvgpr  6760  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemloc  6773  caucvgprlemcl  6774  caucvgprlemladdfu  6775  caucvgprlemladdrl  6776  caucvgprlem2  6778  caucvgpr  6780  caucvgprprlemelu  6784  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemmu  6793  caucvgprprlemopu  6797  caucvgprprlemloc  6801  caucvgprprlemclphr  6803  caucvgprprlemexbt  6804  caucvgprprlem2  6808  mulcmpblnrlemg  6825  mulsrmo  6829  mulsrpr  6831  mulcomsrg  6842  distrsrg  6844  recexgt0sr  6858  mulgt0sr  6862  mulextsr1lem  6864  caucvgsrlemgt1  6879  caucvgsr  6886  addcnsr  6910  mulcnsr  6911  recidpirqlemcalc  6933  axaddcl  6940  axmulcl  6942  axmulcom  6945  axmulass  6947  axdistr  6948  axcaucvglemcau  6972  axcaucvglemres  6973  adddir  7018  muladd11  7146  1p1times  7147  pnpcan2  7251  muladd  7381  subdir  7383  mulsub  7398  mulreim  7595  apadd1  7599  mulext1  7603  recextlem1  7632  muleqadd  7649  divdirap  7674  divadddivap  7703  conjmulap  7705  divcanap5rd  7792  div4p1lem1div2  8177  cnref1o  8582  icoshftf1o  8859  lincmb01cmp  8871  iccf1o  8872  fz01en  8917  fzrev3  8949  fzrevral2  8968  fzrevral3  8969  fzshftral  8970  fzoaddel2  9049  fzosubel  9050  fzosubel2  9051  fzocatel  9055  frecuzrdgsuc  9201  frecfzen2  9204  iseqovex  9219  iseqcaopr3  9240  iseqid3s  9246  iseqdistr  9249  serile  9253  mulexp  9294  mulexpzap  9295  expaddzap  9299  expubnd  9311  subsq  9358  binom2  9362  binom21  9363  binom2sub  9364  binom3  9366  crre  9457  replim  9459  remullem  9471  remul2  9473  immul2  9480  cjcj  9483  cjadd  9484  ipcnval  9486  cjmulval  9488  cjneg  9490  imval2  9494  cjreim  9503  cvg1nlemcau  9583  cvg1nlemres  9584  resqrexlemp1rp  9604  resqrexlemfp1  9607  resqrexlemcalc1  9612  resqrexlemcalc2  9613  resqrex  9624  sqabsadd  9653  sqabssub  9654  absreimsq  9665  recan  9705  amgm2  9714  subcn2  9832  climle  9854  climcvg1nlem  9868  serif0  9871