Theorem oveq12d 5708

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 5699	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	syl2anc 404	1 |- ( ph -> ( A F C ) = ( B F D ) )

Syntax hints:   -> wi 4   = wceq 1296  (class class class)co 5690

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-rex 2376  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-br 3868  df-iota 5014  df-fv 5057  df-ov 5693

This theorem is referenced by:  oveq123d  5711  ovmpt2dxf  5808  ovmpt2df  5814  caovdig  5857  caovdir2d  5859  caovdirg  5860  caovdilemd  5874  caovlem2d  5875  offval  5901  fnofval  5903  offval2  5908  ofco  5911  caofinvl  5915  offres  5944  nnmsucr  6289  nndir  6291  ecovdi  6443  ecovidi  6444  dfplpq2  7010  dfmpq2  7011  addcmpblnq  7023  mulpipqqs  7029  addassnqg  7038  distrnqg  7043  ltaddnq  7063  halfnqq  7066  enq0tr  7090  addcmpblnq0  7099  addnq0mo  7103  addnnnq0  7105  nqnq0a  7110  distrnq0  7115  addassnq0  7118  distnq0r  7119  nq02m  7121  ltexpri  7269  cauappcvgprlemm  7301  cauappcvgprlemloc  7308  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  cauappcvgprlem1  7315  cauappcvgprlem2  7316  cauappcvgprlemlim  7317  cauappcvgpr  7318  caucvgprlemnkj  7322  caucvgprlemnbj  7323  caucvgprlemm  7324  caucvgprlemloc  7331  caucvgprlemcl  7332  caucvgprlemladdfu  7333  caucvgprlemladdrl  7334  caucvgprlem2  7336  caucvgpr  7338  caucvgprprlemelu  7342  caucvgprprlemcbv  7343  caucvgprprlemval  7344  caucvgprprlemmu  7351  caucvgprprlemopu  7355  caucvgprprlemloc  7359  caucvgprprlemclphr  7361  caucvgprprlemexbt  7362  caucvgprprlem2  7366  mulcmpblnrlemg  7383  mulsrmo  7387  mulsrpr  7389  mulcomsrg  7400  distrsrg  7402  recexgt0sr  7416  mulgt0sr  7420  mulextsr1lem  7422  caucvgsrlemgt1  7437  caucvgsr  7444  addcnsr  7468  mulcnsr  7469  recidpirqlemcalc  7491  axaddcl  7498  axmulcl  7500  axmulcom  7503  axmulass  7505  axdistr  7506  axcaucvglemcau  7530  axcaucvglemres  7531  adddir  7576  muladd11  7712  1p1times  7713  muladd11r  7735  pnpcan2  7819  muladd  7959  subdir  7961  mulsub  7976  mulreim  8178  apadd1  8182  mulext1  8186  recextlem1  8217  muleqadd  8234  divdirap  8261  divadddivap  8291  conjmulap  8293  divcanap5rd  8382  xp1d2m1eqxm1d2  8766  div4p1lem1div2  8767  cnref1o  9232  xnegid  9425  xposdif  9448  xleaddadd  9453  icoshftf1o  9557  lincmb01cmp  9569  iccf1o  9570  fz01en  9616  fzrev3  9650  fzrevral2  9669  fzrevral3  9670  fzshftral  9671  fzoaddel2  9753  fzosubel  9754  fzosubel2  9755  fzocatel  9759  modqsubdir  9949  addmodlteq  9954  frecuzrdgsuc  9970  frecfzen2  9983  iseqovex  10011  seq3caopr3  10031  seq3f1olemqsumkj  10048  seq3f1olemqsumk  10049  seq3f1olemqsum  10050  seq3id3  10057  seqfeq3  10062  seq3distr  10063  ser3le  10068  mulexp  10109  mulexpzap  10110  expaddzap  10114  expubnd  10127  subsq  10176  binom2  10180  binom21  10181  binom2sub  10182  binom2sub1  10183  binom3  10186  sqoddm1div8  10221  nn0opthlem1d  10243  nn0opthd  10245  facp1  10253  facubnd  10268  bcval  10272  bcn1  10281  bcm1k  10283  bcp1n  10284  bcp1nk  10285  bcval5  10286  bcn2  10287  bcpasc  10289  hashun  10328  hashfz  10344  crre  10406  replim  10408  remullem  10420  remul2  10422  immul2  10429  cjcj  10432  cjadd  10433  ipcnval  10435  cjmulval  10437  cjneg  10439  imval2  10443  cjreim  10452  cvg1nlemcau  10532  cvg1nlemres  10533  resqrexlemp1rp  10554  resqrexlemfp1  10557  resqrexlemcalc1  10562  resqrexlemcalc2  10563  resqrex  10574  sqabsadd  10603  sqabssub  10604  absreimsq  10615  recan  10657  amgm2  10666  maxabslemab  10754  maxabslemval  10756  max0addsup  10767  minabs  10782  bdtrilem  10785  bdtri  10786  xrmaxadd  10804  xrminadd  10818  xrbdtri  10819  subcn2  10854  reccn2ap  10856  climle  10877  climcvg1nlem  10892  serf0  10895  fsumadd  10949  fsumsplit  10950  sumpr  10956  sumtp  10957  isumadd  10974  sumsplitdc  10975  fsum2dlemstep  10977  fsumshftm  10988  fisumrev2  10989  fsumconst  10997  modfsummodlemstep  11000  telfsumo  11009  fsumparts  11013  binomlem  11026  binom  11027  binom1dif  11030  bcxmaslem1  11031  isumsplit  11034  isumnn0nn  11036  arisum  11041  arisum2  11042  trireciplem  11043  trirecip  11044  geosergap  11049  geo2sum  11057  geo2sum2  11058  cvgratnnlemsumlt  11071  mertenslemi1  11078  mertensabs  11080  eftabs  11095  eftvalcn  11096  efcllemp  11097  ege2le3  11110  efcj  11112  efaddlem  11113  efsep  11130  ef4p  11133  efgt1p2  11134  efgt1p  11135  sinval  11142  cosval  11143  tanvalap  11148  tanval2ap  11153  tanval3ap  11154  efi4p  11157  sinneg  11166  cosneg  11167  tannegap  11168  efival  11172  efmival  11173  sinadd  11176  cosadd  11177  tanaddaplem  11178  tanaddap  11179  sinsub  11180  cossub  11181  addsin  11182  subsin  11183  sinmul  11184  cosmul  11185  addcos  11186  subcos  11187  sincossq  11188  cos2t  11190  sin01bnd  11197  cos01bnd  11198  efieq1re  11210  demoivreALT  11212  dvds2ln  11256  odd2np1lem  11299  gcdaddm  11402  bezoutlemnewy  11412  dfgcd3  11426  dvdsgcd  11428  mulgcd  11432  mulgcdr  11434  gcddiv  11435  sqgcd  11445  lcmgcdlem  11486  lcmgcd  11487  qredeu  11506  divgcdcoprm0  11510  cncongr1  11512  oddpwdclemdc  11578  sqrt2irraplemnn  11584  qnumdenbi  11597  zgcdsq  11606  hashdvds  11624  phiprmpw  11625  phimullem  11628  ressid2  11702  ressval2  11703  topnvalg  11816  topnpropgd  11818  cnfval  12046  cnpfval  12047  ispsmet  12109  psmet0  12113  psmettri2  12114  psmetres2  12119  ismet  12130  isxmet  12131  xmettri2  12147  xmetres2  12165  xblss2  12191  xmstri2  12256  mstri2  12257  xmstri  12258  mstri  12259  xmstri3  12260  mstri3  12261  msrtri  12262  comet  12285  bdxmet  12287  cnmet  12309  ioo2bl  12319  elcncf  12328  mulc1cncf  12344  cncfco  12346  cncfmptc  12348  cncfmptid  12349  addccncf  12351  cdivcncfap  12352  negcncf  12353  mulcncflem  12355