Theorem oveq12d 5895

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

Syntax hints:   -> wi 4   = wceq 1353  (class class class)co 5877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2741  df-un 3135  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880

This theorem is referenced by:  oveq123d  5898  ovmpodxf  6002  ovmpodf  6008  caovdig  6051  caovdir2d  6053  caovdirg  6054  caovdilemd  6068  caovlem2d  6069  offval  6092  ofvalg  6094  offval2  6100  ofco  6103  caofinvl  6107  offres  6138  nnmsucr  6491  nndir  6493  ecovdi  6648  ecovidi  6649  dfplpq2  7355  dfmpq2  7356  addcmpblnq  7368  mulpipqqs  7374  addassnqg  7383  distrnqg  7388  ltaddnq  7408  halfnqq  7411  enq0tr  7435  addcmpblnq0  7444  addnq0mo  7448  addnnnq0  7450  nqnq0a  7455  distrnq0  7460  addassnq0  7463  distnq0r  7464  nq02m  7466  ltexpri  7614  cauappcvgprlemm  7646  cauappcvgprlemloc  7653  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlem1  7660  cauappcvgprlem2  7661  cauappcvgprlemlim  7662  cauappcvgpr  7663  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemm  7669  caucvgprlemloc  7676  caucvgprlemcl  7677  caucvgprlemladdfu  7678  caucvgprlemladdrl  7679  caucvgprlem2  7681  caucvgpr  7683  caucvgprprlemelu  7687  caucvgprprlemcbv  7688  caucvgprprlemval  7689  caucvgprprlemmu  7696  caucvgprprlemopu  7700  caucvgprprlemloc  7704  caucvgprprlemclphr  7706  caucvgprprlemexbt  7707  caucvgprprlem2  7711  mulcmpblnrlemg  7741  mulsrmo  7745  mulsrpr  7747  mulcomsrg  7758  distrsrg  7760  recexgt0sr  7774  mulgt0sr  7779  mulextsr1lem  7781  caucvgsrlemgt1  7796  caucvgsr  7803  addcnsr  7835  mulcnsr  7836  recidpirqlemcalc  7858  axaddcl  7865  axmulcl  7867  axmulcom  7872  axmulass  7874  axdistr  7875  axcaucvglemcau  7899  axcaucvglemres  7900  adddir  7950  muladd11  8092  1p1times  8093  muladd11r  8115  pnpcan2  8199  muladd  8343  subdir  8345  mulsub  8360  mulreim  8563  apadd1  8567  mulext1  8571  recextlem1  8610  muleqadd  8627  divdirap  8656  divadddivap  8686  conjmulap  8688  divcanap5rd  8777  subrecap  8798  xp1d2m1eqxm1d2  9173  div4p1lem1div2  9174  cnref1o  9652  xnegid  9861  xposdif  9884  xleaddadd  9889  icoshftf1o  9993  lincmb01cmp  10005  iccf1o  10006  fz01en  10055  fzrev3  10089  fzrevral2  10108  fzrevral3  10109  fzshftral  10110  fzoaddel2  10195  fzosubel  10196  fzosubel2  10197  fzocatel  10201  modqsubdir  10395  addmodlteq  10400  frecuzrdgsuc  10416  frecfzen2  10429  iseqovex  10458  seqvalcd  10461  seq3caopr3  10483  seq3f1olemqsumkj  10500  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  seq3id3  10509  seqfeq3  10514  seq3distr  10515  ser3le  10520  mulexp  10561  mulexpzap  10562  expaddzap  10566  expubnd  10579  subsq  10629  binom2  10634  binom21  10635  binom2sub  10636  binom2sub1  10637  binom3  10640  sqoddm1div8  10676  mulsubdivbinom2ap  10693  nn0opthlem1d  10702  nn0opthd  10704  facp1  10712  facubnd  10727  bcval  10731  bcn1  10740  bcm1k  10742  bcp1n  10743  bcp1nk  10744  bcval5  10745  bcn2  10746  bcpasc  10748  hashun  10787  hashfz  10803  crre  10868  replim  10870  remullem  10882  remul2  10884  immul2  10891  cjcj  10894  cjadd  10895  ipcnval  10897  cjmulval  10899  cjneg  10901  imval2  10905  cjreim  10914  cvg1nlemcau  10995  cvg1nlemres  10996  resqrexlemp1rp  11017  resqrexlemfp1  11020  resqrexlemcalc1  11025  resqrexlemcalc2  11026  resqrex  11037  sqabsadd  11066  sqabssub  11067  absreimsq  11078  recan  11120  amgm2  11129  maxabslemab  11217  maxabslemval  11219  max0addsup  11230  minabs  11246  bdtrilem  11249  bdtri  11250  xrmaxadd  11271  xrminadd  11285  xrbdtri  11286  subcn2  11321  reccn2ap  11323  climle  11344  climcvg1nlem  11359  serf0  11362  fsumadd  11416  fsumsplit  11417  sumpr  11423  sumtp  11424  isumadd  11441  sumsplitdc  11442  fsum2dlemstep  11444  fsumshftm  11455  fisumrev2  11456  fsumconst  11464  modfsummodlemstep  11467  telfsumo  11476  fsumparts  11480  binomlem  11493  binom  11494  binom1dif  11497  bcxmaslem1  11498  isumsplit  11501  isumnn0nn  11503  arisum  11508  arisum2  11509  trireciplem  11510  trirecip  11511  geosergap  11516  geo2sum  11524  geo2sum2  11525  cvgratnnlemsumlt  11538  mertenslemi1  11545  mertensabs  11547  fprodmul  11601  fprodsplitdc  11606  fprodabs  11626  fprod2dlemstep  11632  fproddivapf  11641  eftabs  11666  eftvalcn  11667  efcllemp  11668  ege2le3  11681  efcj  11683  efaddlem  11684  efsep  11701  ef4p  11704  efgt1p2  11705  efgt1p  11706  sinval  11712  cosval  11713  tanvalap  11718  tanval2ap  11723  tanval3ap  11724  efi4p  11727  sinneg  11736  cosneg  11737  tannegap  11738  efival  11742  efmival  11743  sinadd  11746  cosadd  11747  tanaddaplem  11748  tanaddap  11749  sinsub  11750  cossub  11751  addsin  11752  subsin  11753  sinmul  11754  cosmul  11755  addcos  11756  subcos  11757  sincossq  11758  cos2t  11760  sin01bnd  11767  cos01bnd  11768  efieq1re  11781  demoivreALT  11783  dvds2ln  11833  odd2np1lem  11879  gcdaddm  11987  bezoutlemnewy  11999  dfgcd3  12013  dvdsgcd  12015  mulgcd  12019  mulgcdr  12021  gcddiv  12022  sqgcd  12032  lcmgcdlem  12079  lcmgcd  12080  qredeu  12099  divgcdcoprm0  12103  cncongr1  12105  oddpwdclemdc  12175  sqrt2irraplemnn  12181  qnumdenbi  12194  zgcdsq  12203  hashdvds  12223  phiprmpw  12224  phimullem  12227  eulerthlema  12232  prmdiv  12237  modprm0  12256  coprimeprodsq  12259  pythagtriplem1  12267  pythagtriplem12  12277  pythagtriplem14  12279  pythagtriplem15  12280  pythagtriplem16  12281  pythagtriplem17  12282  pythagtriplem19  12284  pcval  12298  pcmul  12303  pcdiv  12304  pcqmul  12305  pcid  12325  pcaddlem  12340  pcmpt  12343  pcmpt2  12344  pcmptdvds  12345  pcbc  12351  4sqlem4  12392  mul4sqlem  12393  mul4sq  12394  ennnfonelemp1  12409  nninfdclemp1  12453  ressvalsets  12526  topnvalg  12705  topnpropgd  12707  prdsex  12723  qusval  12749  qusaddvallemg  12757  xpsval  12776  ismhm  12858  mhmf1o  12866  0mhm  12878  mhmco  12879  mhmeql  12881  isgrpid2  12918  grpnpcan  12967  mhmmnd  12985  mulgnndir  13017  mulgdir  13020  isnsg3  13072  ablsub4  13121  mgpvalg  13138  mgptopng  13144  mgpress  13146  srglmhm  13181  srgrmhm  13182  ringo2times  13216  ringcom  13219  ringpropd  13222  ring1  13241  opprvalg  13246  opprring  13254  invrfvald  13296  dvrvald  13308  dvrdir  13317  rdivmuldivd  13318  islmod  13386  lmodlema  13387  islmodd  13388  lmodcom  13428  lmodnegadd  13431  lmodprop2d  13443  rmodislmod  13446  lsssn0  13461  cnfval  13733  cnpfval  13734  ispsmet  13862  psmet0  13866  psmettri2  13867  psmetres2  13872  ismet  13883  isxmet  13884  xmettri2  13900  xmetres2  13918  xblss2  13944  xmstri2  14009  mstri2  14010  xmstri  14011  mstri  14012  xmstri3  14013  mstri3  14014  msrtri  14015  comet  14038  bdxmet  14040  txmetcnp  14057  metcnpd  14059  cnmet  14069  ioo2bl  14082  fsumcncntop  14095  elcncf  14099  mulc1cncf  14115  cncfco  14117  cncfcncntop  14119  cncfmptc  14121  cncfmptid  14122  addccncf  14125  cdivcncfap  14126  negcncf  14127  mulcncflem  14129  limccnp2cntop  14185  reldvg  14187  dvfvalap  14189  eldvap  14190  dvconst  14200  dvaddxxbr  14204  dvmulxxbr  14205  dvcoapbr  14210  dvcjbr  14211  dvexp  14214  dvrecap  14216  dveflem  14226  dvef  14227  sinperlem  14268  sinmpi  14275  cosmpi  14276  sinppi  14277  cosppi  14278  efimpi  14279  sinhalfpip  14280  sinhalfpim  14281  coshalfpip  14282  coshalfpim  14283  ptolemy  14284  tangtx  14298  logdivlti  14341  rpcxpadd  14365  rpmulcxp  14369  rplogbchbase  14407  rprelogbmul  14412  binom4  14436  lgsval  14444  lgsfvalg  14445  lgsval2lem  14450  lgsval4a  14462  lgsneg  14464  lgsdilem  14467  lgsdirprm  14474  lgsdir  14475  lgsdilem2  14476  lgsdi  14477  lgsne0  14478  lgseisenlem2  14490  2sqlem2  14501  2sqlem3  14503  2sqlem4  14504  2sqlem8  14509  cvgcmp2nlemabs  14819  trilpolemclim  14823  trilpolemcl  14824  trilpolemisumle  14825  trilpolemeq1  14827  trilpolemlt1  14828  trilpo  14830  redcwlpo  14842  nconstwlpolemgt0  14851  nconstwlpo  14853  neapmkv  14855