Theorem oveq12d 5800

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

Syntax hints:   -> wi 4   = wceq 1332  (class class class)co 5782

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785

This theorem is referenced by:  oveq123d  5803  ovmpodxf  5904  ovmpodf  5910  caovdig  5953  caovdir2d  5955  caovdirg  5956  caovdilemd  5970  caovlem2d  5971  offval  5997  ofvalg  5999  offval2  6005  ofco  6008  caofinvl  6012  offres  6041  nnmsucr  6392  nndir  6394  ecovdi  6548  ecovidi  6549  dfplpq2  7186  dfmpq2  7187  addcmpblnq  7199  mulpipqqs  7205  addassnqg  7214  distrnqg  7219  ltaddnq  7239  halfnqq  7242  enq0tr  7266  addcmpblnq0  7275  addnq0mo  7279  addnnnq0  7281  nqnq0a  7286  distrnq0  7291  addassnq0  7294  distnq0r  7295  nq02m  7297  ltexpri  7445  cauappcvgprlemm  7477  cauappcvgprlemloc  7484  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  cauappcvgprlem2  7492  cauappcvgprlemlim  7493  cauappcvgpr  7494  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemm  7500  caucvgprlemloc  7507  caucvgprlemcl  7508  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprlem2  7512  caucvgpr  7514  caucvgprprlemelu  7518  caucvgprprlemcbv  7519  caucvgprprlemval  7520  caucvgprprlemmu  7527  caucvgprprlemopu  7531  caucvgprprlemloc  7535  caucvgprprlemclphr  7537  caucvgprprlemexbt  7538  caucvgprprlem2  7542  mulcmpblnrlemg  7572  mulsrmo  7576  mulsrpr  7578  mulcomsrg  7589  distrsrg  7591  recexgt0sr  7605  mulgt0sr  7610  mulextsr1lem  7612  caucvgsrlemgt1  7627  caucvgsr  7634  addcnsr  7666  mulcnsr  7667  recidpirqlemcalc  7689  axaddcl  7696  axmulcl  7698  axmulcom  7703  axmulass  7705  axdistr  7706  axcaucvglemcau  7730  axcaucvglemres  7731  adddir  7781  muladd11  7919  1p1times  7920  muladd11r  7942  pnpcan2  8026  muladd  8170  subdir  8172  mulsub  8187  mulreim  8390  apadd1  8394  mulext1  8398  recextlem1  8436  muleqadd  8453  divdirap  8481  divadddivap  8511  conjmulap  8513  divcanap5rd  8602  subrecap  8622  xp1d2m1eqxm1d2  8996  div4p1lem1div2  8997  cnref1o  9469  xnegid  9672  xposdif  9695  xleaddadd  9700  icoshftf1o  9804  lincmb01cmp  9816  iccf1o  9817  fz01en  9864  fzrev3  9898  fzrevral2  9917  fzrevral3  9918  fzshftral  9919  fzoaddel2  10001  fzosubel  10002  fzosubel2  10003  fzocatel  10007  modqsubdir  10197  addmodlteq  10202  frecuzrdgsuc  10218  frecfzen2  10231  iseqovex  10260  seqvalcd  10263  seq3caopr3  10285  seq3f1olemqsumkj  10302  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  seq3id3  10311  seqfeq3  10316  seq3distr  10317  ser3le  10322  mulexp  10363  mulexpzap  10364  expaddzap  10368  expubnd  10381  subsq  10430  binom2  10434  binom21  10435  binom2sub  10436  binom2sub1  10437  binom3  10440  sqoddm1div8  10475  nn0opthlem1d  10498  nn0opthd  10500  facp1  10508  facubnd  10523  bcval  10527  bcn1  10536  bcm1k  10538  bcp1n  10539  bcp1nk  10540  bcval5  10541  bcn2  10542  bcpasc  10544  hashun  10583  hashfz  10599  crre  10661  replim  10663  remullem  10675  remul2  10677  immul2  10684  cjcj  10687  cjadd  10688  ipcnval  10690  cjmulval  10692  cjneg  10694  imval2  10698  cjreim  10707  cvg1nlemcau  10788  cvg1nlemres  10789  resqrexlemp1rp  10810  resqrexlemfp1  10813  resqrexlemcalc1  10818  resqrexlemcalc2  10819  resqrex  10830  sqabsadd  10859  sqabssub  10860  absreimsq  10871  recan  10913  amgm2  10922  maxabslemab  11010  maxabslemval  11012  max0addsup  11023  minabs  11039  bdtrilem  11042  bdtri  11043  xrmaxadd  11062  xrminadd  11076  xrbdtri  11077  subcn2  11112  reccn2ap  11114  climle  11135  climcvg1nlem  11150  serf0  11153  fsumadd  11207  fsumsplit  11208  sumpr  11214  sumtp  11215  isumadd  11232  sumsplitdc  11233  fsum2dlemstep  11235  fsumshftm  11246  fisumrev2  11247  fsumconst  11255  modfsummodlemstep  11258  telfsumo  11267  fsumparts  11271  binomlem  11284  binom  11285  binom1dif  11288  bcxmaslem1  11289  isumsplit  11292  isumnn0nn  11294  arisum  11299  arisum2  11300  trireciplem  11301  trirecip  11302  geosergap  11307  geo2sum  11315  geo2sum2  11316  cvgratnnlemsumlt  11329  mertenslemi1  11336  mertensabs  11338  eftabs  11399  eftvalcn  11400  efcllemp  11401  ege2le3  11414  efcj  11416  efaddlem  11417  efsep  11434  ef4p  11437  efgt1p2  11438  efgt1p  11439  sinval  11445  cosval  11446  tanvalap  11451  tanval2ap  11456  tanval3ap  11457  efi4p  11460  sinneg  11469  cosneg  11470  tannegap  11471  efival  11475  efmival  11476  sinadd  11479  cosadd  11480  tanaddaplem  11481  tanaddap  11482  sinsub  11483  cossub  11484  addsin  11485  subsin  11486  sinmul  11487  cosmul  11488  addcos  11489  subcos  11490  sincossq  11491  cos2t  11493  sin01bnd  11500  cos01bnd  11501  efieq1re  11514  demoivreALT  11516  dvds2ln  11562  odd2np1lem  11605  gcdaddm  11708  bezoutlemnewy  11720  dfgcd3  11734  dvdsgcd  11736  mulgcd  11740  mulgcdr  11742  gcddiv  11743  sqgcd  11753  lcmgcdlem  11794  lcmgcd  11795  qredeu  11814  divgcdcoprm0  11818  cncongr1  11820  oddpwdclemdc  11887  sqrt2irraplemnn  11893  qnumdenbi  11906  zgcdsq  11915  hashdvds  11933  phiprmpw  11934  phimullem  11937  ennnfonelemp1  11955  ressid2  12057  ressval2  12058  topnvalg  12171  topnpropgd  12173  cnfval  12402  cnpfval  12403  ispsmet  12531  psmet0  12535  psmettri2  12536  psmetres2  12541  ismet  12552  isxmet  12553  xmettri2  12569  xmetres2  12587  xblss2  12613  xmstri2  12678  mstri2  12679  xmstri  12680  mstri  12681  xmstri3  12682  mstri3  12683  msrtri  12684  comet  12707  bdxmet  12709  txmetcnp  12726  metcnpd  12728  cnmet  12738  ioo2bl  12751  fsumcncntop  12764  elcncf  12768  mulc1cncf  12784  cncfco  12786  cncfcncntop  12788  cncfmptc  12790  cncfmptid  12791  addccncf  12794  cdivcncfap  12795  negcncf  12796  mulcncflem  12798  limccnp2cntop  12854  reldvg  12856  dvfvalap  12858  eldvap  12859  dvconst  12869  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879  dvcjbr  12880  dvexp  12883  dvrecap  12885  dveflem  12895  dvef  12896  sinperlem  12937  sinmpi  12944  cosmpi  12945  sinppi  12946  cosppi  12947  efimpi  12948  sinhalfpip  12949  sinhalfpim  12950  coshalfpip  12951  coshalfpim  12952  ptolemy  12953  tangtx  12967  logdivlti  13010  rpcxpadd  13034  rpmulcxp  13038  rplogbchbase  13075  rprelogbmul  13080  cvgcmp2nlemabs  13402  trilpolemclim  13404  trilpolemcl  13405  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409  trilpo  13411  redcwlpo  13422  neapmkv  13425