Theorem oveq12d 5868

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 5859	. 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 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:  oveq123d  5871  ovmpodxf  5975  ovmpodf  5981  caovdig  6024  caovdir2d  6026  caovdirg  6027  caovdilemd  6041  caovlem2d  6042  offval  6065  ofvalg  6067  offval2  6073  ofco  6076  caofinvl  6080  offres  6111  nnmsucr  6464  nndir  6466  ecovdi  6620  ecovidi  6621  dfplpq2  7303  dfmpq2  7304  addcmpblnq  7316  mulpipqqs  7322  addassnqg  7331  distrnqg  7336  ltaddnq  7356  halfnqq  7359  enq0tr  7383  addcmpblnq0  7392  addnq0mo  7396  addnnnq0  7398  nqnq0a  7403  distrnq0  7408  addassnq0  7411  distnq0r  7412  nq02m  7414  ltexpri  7562  cauappcvgprlemm  7594  cauappcvgprlemloc  7601  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  cauappcvgprlem1  7608  cauappcvgprlem2  7609  cauappcvgprlemlim  7610  cauappcvgpr  7611  caucvgprlemnkj  7615  caucvgprlemnbj  7616  caucvgprlemm  7617  caucvgprlemloc  7624  caucvgprlemcl  7625  caucvgprlemladdfu  7626  caucvgprlemladdrl  7627  caucvgprlem2  7629  caucvgpr  7631  caucvgprprlemelu  7635  caucvgprprlemcbv  7636  caucvgprprlemval  7637  caucvgprprlemmu  7644  caucvgprprlemopu  7648  caucvgprprlemloc  7652  caucvgprprlemclphr  7654  caucvgprprlemexbt  7655  caucvgprprlem2  7659  mulcmpblnrlemg  7689  mulsrmo  7693  mulsrpr  7695  mulcomsrg  7706  distrsrg  7708  recexgt0sr  7722  mulgt0sr  7727  mulextsr1lem  7729  caucvgsrlemgt1  7744  caucvgsr  7751  addcnsr  7783  mulcnsr  7784  recidpirqlemcalc  7806  axaddcl  7813  axmulcl  7815  axmulcom  7820  axmulass  7822  axdistr  7823  axcaucvglemcau  7847  axcaucvglemres  7848  adddir  7898  muladd11  8039  1p1times  8040  muladd11r  8062  pnpcan2  8146  muladd  8290  subdir  8292  mulsub  8307  mulreim  8510  apadd1  8514  mulext1  8518  recextlem1  8556  muleqadd  8573  divdirap  8601  divadddivap  8631  conjmulap  8633  divcanap5rd  8722  subrecap  8743  xp1d2m1eqxm1d2  9117  div4p1lem1div2  9118  cnref1o  9596  xnegid  9803  xposdif  9826  xleaddadd  9831  icoshftf1o  9935  lincmb01cmp  9947  iccf1o  9948  fz01en  9996  fzrev3  10030  fzrevral2  10049  fzrevral3  10050  fzshftral  10051  fzoaddel2  10136  fzosubel  10137  fzosubel2  10138  fzocatel  10142  modqsubdir  10336  addmodlteq  10341  frecuzrdgsuc  10357  frecfzen2  10370  iseqovex  10399  seqvalcd  10402  seq3caopr3  10424  seq3f1olemqsumkj  10441  seq3f1olemqsumk  10442  seq3f1olemqsum  10443  seq3id3  10450  seqfeq3  10455  seq3distr  10456  ser3le  10461  mulexp  10502  mulexpzap  10503  expaddzap  10507  expubnd  10520  subsq  10569  binom2  10574  binom21  10575  binom2sub  10576  binom2sub1  10577  binom3  10580  sqoddm1div8  10616  nn0opthlem1d  10641  nn0opthd  10643  facp1  10651  facubnd  10666  bcval  10670  bcn1  10679  bcm1k  10681  bcp1n  10682  bcp1nk  10683  bcval5  10684  bcn2  10685  bcpasc  10687  hashun  10727  hashfz  10743  crre  10808  replim  10810  remullem  10822  remul2  10824  immul2  10831  cjcj  10834  cjadd  10835  ipcnval  10837  cjmulval  10839  cjneg  10841  imval2  10845  cjreim  10854  cvg1nlemcau  10935  cvg1nlemres  10936  resqrexlemp1rp  10957  resqrexlemfp1  10960  resqrexlemcalc1  10965  resqrexlemcalc2  10966  resqrex  10977  sqabsadd  11006  sqabssub  11007  absreimsq  11018  recan  11060  amgm2  11069  maxabslemab  11157  maxabslemval  11159  max0addsup  11170  minabs  11186  bdtrilem  11189  bdtri  11190  xrmaxadd  11211  xrminadd  11225  xrbdtri  11226  subcn2  11261  reccn2ap  11263  climle  11284  climcvg1nlem  11299  serf0  11302  fsumadd  11356  fsumsplit  11357  sumpr  11363  sumtp  11364  isumadd  11381  sumsplitdc  11382  fsum2dlemstep  11384  fsumshftm  11395  fisumrev2  11396  fsumconst  11404  modfsummodlemstep  11407  telfsumo  11416  fsumparts  11420  binomlem  11433  binom  11434  binom1dif  11437  bcxmaslem1  11438  isumsplit  11441  isumnn0nn  11443  arisum  11448  arisum2  11449  trireciplem  11450  trirecip  11451  geosergap  11456  geo2sum  11464  geo2sum2  11465  cvgratnnlemsumlt  11478  mertenslemi1  11485  mertensabs  11487  fprodmul  11541  fprodsplitdc  11546  fprodabs  11566  fprod2dlemstep  11572  fproddivapf  11581  eftabs  11606  eftvalcn  11607  efcllemp  11608  ege2le3  11621  efcj  11623  efaddlem  11624  efsep  11641  ef4p  11644  efgt1p2  11645  efgt1p  11646  sinval  11652  cosval  11653  tanvalap  11658  tanval2ap  11663  tanval3ap  11664  efi4p  11667  sinneg  11676  cosneg  11677  tannegap  11678  efival  11682  efmival  11683  sinadd  11686  cosadd  11687  tanaddaplem  11688  tanaddap  11689  sinsub  11690  cossub  11691  addsin  11692  subsin  11693  sinmul  11694  cosmul  11695  addcos  11696  subcos  11697  sincossq  11698  cos2t  11700  sin01bnd  11707  cos01bnd  11708  efieq1re  11721  demoivreALT  11723  dvds2ln  11773  odd2np1lem  11818  gcdaddm  11926  bezoutlemnewy  11938  dfgcd3  11952  dvdsgcd  11954  mulgcd  11958  mulgcdr  11960  gcddiv  11961  sqgcd  11971  lcmgcdlem  12018  lcmgcd  12019  qredeu  12038  divgcdcoprm0  12042  cncongr1  12044  oddpwdclemdc  12114  sqrt2irraplemnn  12120  qnumdenbi  12133  zgcdsq  12142  hashdvds  12162  phiprmpw  12163  phimullem  12166  eulerthlema  12171  prmdiv  12176  modprm0  12195  coprimeprodsq  12198  pythagtriplem1  12206  pythagtriplem12  12216  pythagtriplem14  12218  pythagtriplem15  12219  pythagtriplem16  12220  pythagtriplem17  12221  pythagtriplem19  12223  pcval  12237  pcmul  12242  pcdiv  12243  pcqmul  12244  pcid  12264  pcaddlem  12279  pcmpt  12282  pcmpt2  12283  pcmptdvds  12284  pcbc  12290  4sqlem4  12331  mul4sqlem  12332  mul4sq  12333  ennnfonelemp1  12348  nninfdclemp1  12392  ressid2  12464  ressval2  12465  topnvalg  12578  topnpropgd  12580  ismhm  12672  mhmf1o  12680  0mhm  12691  mhmco  12692  mhmeql  12694  isgrpid2  12730  cnfval  12947  cnpfval  12948  ispsmet  13076  psmet0  13080  psmettri2  13081  psmetres2  13086  ismet  13097  isxmet  13098  xmettri2  13114  xmetres2  13132  xblss2  13158  xmstri2  13223  mstri2  13224  xmstri  13225  mstri  13226  xmstri3  13227  mstri3  13228  msrtri  13229  comet  13252  bdxmet  13254  txmetcnp  13271  metcnpd  13273  cnmet  13283  ioo2bl  13296  fsumcncntop  13309  elcncf  13313  mulc1cncf  13329  cncfco  13331  cncfcncntop  13333  cncfmptc  13335  cncfmptid  13336  addccncf  13339  cdivcncfap  13340  negcncf  13341  mulcncflem  13343  limccnp2cntop  13399  reldvg  13401  dvfvalap  13403  eldvap  13404  dvconst  13414  dvaddxxbr  13418  dvmulxxbr  13419  dvcoapbr  13424  dvcjbr  13425  dvexp  13428  dvrecap  13430  dveflem  13440  dvef  13441  sinperlem  13482  sinmpi  13489  cosmpi  13490  sinppi  13491  cosppi  13492  efimpi  13493  sinhalfpip  13494  sinhalfpim  13495  coshalfpip  13496  coshalfpim  13497  ptolemy  13498  tangtx  13512  logdivlti  13555  rpcxpadd  13579  rpmulcxp  13583  rplogbchbase  13621  rprelogbmul  13626  binom4  13650  lgsval  13658  lgsfvalg  13659  lgsval2lem  13664  lgsval4a  13676  lgsneg  13678  lgsdilem  13681  lgsdirprm  13688  lgsdir  13689  lgsdilem2  13690  lgsdi  13691  lgsne0  13692  2sqlem2  13704  2sqlem3  13706  2sqlem4  13707  2sqlem8  13712  cvgcmp2nlemabs  14024  trilpolemclim  14028  trilpolemcl  14029  trilpolemisumle  14030  trilpolemeq1  14032  trilpolemlt1  14033  trilpo  14035  redcwlpo  14047  nconstwlpolemgt0  14055  nconstwlpo  14057  neapmkv  14059