Theorem oveq12d 5937

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 5928	. 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 1364  (class class class)co 5919

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-iota 5216  df-fv 5263  df-ov 5922

This theorem is referenced by:  oveq123d  5940  ovmpodxf  6045  ovmpodf  6051  caovdig  6095  caovdir2d  6097  caovdirg  6098  caovdilemd  6112  caovlem2d  6113  offval  6140  ofvalg  6142  offval2  6148  ofco  6151  caofinvl  6157  offres  6189  nnmsucr  6543  nndir  6545  ecovdi  6702  ecovidi  6703  dfplpq2  7416  dfmpq2  7417  addcmpblnq  7429  mulpipqqs  7435  addassnqg  7444  distrnqg  7449  ltaddnq  7469  halfnqq  7472  enq0tr  7496  addcmpblnq0  7505  addnq0mo  7509  addnnnq0  7511  nqnq0a  7516  distrnq0  7521  addassnq0  7524  distnq0r  7525  nq02m  7527  ltexpri  7675  cauappcvgprlemm  7707  cauappcvgprlemloc  7714  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlem2  7722  cauappcvgprlemlim  7723  cauappcvgpr  7724  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem2  7742  caucvgpr  7744  caucvgprprlemelu  7748  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemmu  7757  caucvgprprlemopu  7761  caucvgprprlemloc  7765  caucvgprprlemclphr  7767  caucvgprprlemexbt  7768  caucvgprprlem2  7772  mulcmpblnrlemg  7802  mulsrmo  7806  mulsrpr  7808  mulcomsrg  7819  distrsrg  7821  recexgt0sr  7835  mulgt0sr  7840  mulextsr1lem  7842  caucvgsrlemgt1  7857  caucvgsr  7864  addcnsr  7896  mulcnsr  7897  recidpirqlemcalc  7919  axaddcl  7926  axmulcl  7928  axmulcom  7933  axmulass  7935  axdistr  7936  axcaucvglemcau  7960  axcaucvglemres  7961  adddir  8012  muladd11  8154  1p1times  8155  muladd11r  8177  pnpcan2  8261  muladd  8405  subdir  8407  mulsub  8422  mulreim  8625  apadd1  8629  mulext1  8633  recextlem1  8672  muleqadd  8689  divdirap  8718  divadddivap  8748  conjmulap  8750  divcanap5rd  8839  subrecap  8860  xp1d2m1eqxm1d2  9238  div4p1lem1div2  9239  cnref1o  9719  xnegid  9928  xposdif  9951  xleaddadd  9956  icoshftf1o  10060  lincmb01cmp  10072  iccf1o  10073  fz01en  10122  fzrev3  10156  fzrevral2  10175  fzrevral3  10176  fzshftral  10177  fzoaddel2  10263  fzosubel  10264  fzosubel2  10265  fzocatel  10269  modqsubdir  10467  addmodlteq  10472  frecuzrdgsuc  10488  frecfzen2  10501  iseqovex  10532  seqvalcd  10535  seq3caopr3  10565  seqcaopr3g  10566  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seqf1oglem2  10594  seq3id3  10598  seqfeq3  10603  seq3distr  10606  ser3le  10611  mulexp  10652  mulexpzap  10653  expaddzap  10657  expubnd  10670  subsq  10720  binom2  10725  binom21  10726  binom2sub  10727  binom2sub1  10728  binom3  10731  sqoddm1div8  10767  mulsubdivbinom2ap  10785  nn0opthlem1d  10794  nn0opthd  10796  facp1  10804  facubnd  10819  bcval  10823  bcn1  10832  bcm1k  10834  bcp1n  10835  bcp1nk  10836  bcval5  10837  bcn2  10838  bcpasc  10840  hashun  10879  hashfz  10895  crre  11004  replim  11006  remullem  11018  remul2  11020  immul2  11027  cjcj  11030  cjadd  11031  ipcnval  11033  cjmulval  11035  cjneg  11037  imval2  11041  cjreim  11050  cvg1nlemcau  11131  cvg1nlemres  11132  resqrexlemp1rp  11153  resqrexlemfp1  11156  resqrexlemcalc1  11161  resqrexlemcalc2  11162  resqrex  11173  sqabsadd  11202  sqabssub  11203  absreimsq  11214  recan  11256  amgm2  11265  maxabslemab  11353  maxabslemval  11355  max0addsup  11366  minabs  11382  bdtrilem  11385  bdtri  11386  xrmaxadd  11407  xrminadd  11421  xrbdtri  11422  subcn2  11457  reccn2ap  11459  climle  11480  climcvg1nlem  11495  serf0  11498  fsumadd  11552  fsumsplit  11553  sumpr  11559  sumtp  11560  isumadd  11577  sumsplitdc  11578  fsum2dlemstep  11580  fsumshftm  11591  fisumrev2  11592  fsumconst  11600  modfsummodlemstep  11603  telfsumo  11612  fsumparts  11616  binomlem  11629  binom  11630  binom1dif  11633  bcxmaslem1  11634  isumsplit  11637  isumnn0nn  11639  arisum  11644  arisum2  11645  trireciplem  11646  trirecip  11647  geosergap  11652  geo2sum  11660  geo2sum2  11661  cvgratnnlemsumlt  11674  mertenslemi1  11681  mertensabs  11683  fprodmul  11737  fprodsplitdc  11742  fprodabs  11762  fprod2dlemstep  11768  fproddivapf  11777  eftabs  11802  eftvalcn  11803  efcllemp  11804  ege2le3  11817  efcj  11819  efaddlem  11820  efsep  11837  ef4p  11840  efgt1p2  11841  efgt1p  11842  sinval  11848  cosval  11849  tanvalap  11854  tanval2ap  11859  tanval3ap  11860  efi4p  11863  sinneg  11872  cosneg  11873  tannegap  11874  efival  11878  efmival  11879  sinadd  11882  cosadd  11883  tanaddaplem  11884  tanaddap  11885  sinsub  11886  cossub  11887  addsin  11888  subsin  11889  sinmul  11890  cosmul  11891  addcos  11892  subcos  11893  sincossq  11894  cos2t  11896  sin01bnd  11903  cos01bnd  11904  efieq1re  11918  demoivreALT  11920  dvds2ln  11970  odd2np1lem  12016  gcdaddm  12124  bezoutlemnewy  12136  dfgcd3  12150  dvdsgcd  12152  mulgcd  12156  mulgcdr  12158  gcddiv  12159  sqgcd  12169  lcmgcdlem  12218  lcmgcd  12219  qredeu  12238  divgcdcoprm0  12242  cncongr1  12244  oddpwdclemdc  12314  sqrt2irraplemnn  12320  qnumdenbi  12333  zgcdsq  12342  hashdvds  12362  phiprmpw  12363  phimullem  12366  eulerthlema  12371  prmdiv  12376  modprm0  12395  coprimeprodsq  12398  pythagtriplem1  12406  pythagtriplem12  12416  pythagtriplem14  12418  pythagtriplem15  12419  pythagtriplem16  12420  pythagtriplem17  12421  pythagtriplem19  12423  pcval  12437  pcmul  12442  pcdiv  12443  pcqmul  12444  pcid  12465  pcaddlem  12480  pcmpt  12484  pcmpt2  12485  pcmptdvds  12486  pcbc  12492  4sqlem4  12533  mul4sqlem  12534  mul4sq  12535  4sqlem11  12542  4sqlem12  12543  4sqlem15  12546  4sqlem17  12548  ennnfonelemp1  12566  nninfdclemp1  12610  ressvalsets  12685  topnvalg  12865  topnpropgd  12867  prdsex  12883  qusval  12909  qusex  12911  qusaddvallemg  12919  xpsval  12938  gsumprval  12985  ismhm  13036  mhmf1o  13045  0mhm  13061  mhmco  13065  mhmeql  13067  gsumfzz  13070  isgrpid2  13115  grpnpcan  13167  imasgrp2  13183  mhmmnd  13189  mulgnndir  13224  mulgdir  13227  isnsg3  13280  isghm  13316  ghmnsgima  13341  ghmf1o  13348  conjghm  13349  qusghm  13355  ablsub4  13386  ghmcmn  13400  invghm  13402  gsumfzmptfidmadd  13412  gsumfzconst  13414  mgpvalg  13422  mgptopng  13428  mgpress  13430  rngdi  13439  rngdir  13440  rngpropd  13454  imasrng  13455  srglmhm  13492  srgrmhm  13493  ringo2times  13527  ringcom  13530  ringpropd  13537  ring1  13558  ringlghm  13560  ringrghm  13561  imasring  13563  opprvalg  13568  opprrng  13576  opprring  13578  invrfvald  13621  dvrvald  13633  dvrdir  13642  rdivmuldivd  13643  islmod  13790  lmodlema  13791  islmodd  13792  lmodcom  13832  lmodnegadd  13835  lmodprop2d  13847  rmodislmod  13850  lsssn0  13869  sraval  13936  qusrhm  14027  gsumfzfsumlemm  14086  expghmap  14106  mulgghm2  14107  mulgrhm  14108  zlmval  14126  znval  14135  psrval  14163  cnfval  14373  cnpfval  14374  ispsmet  14502  psmet0  14506  psmettri2  14507  psmetres2  14512  ismet  14523  isxmet  14524  xmettri2  14540  xmetres2  14558  xblss2  14584  xmstri2  14649  mstri2  14650  xmstri  14651  mstri  14652  xmstri3  14653  mstri3  14654  msrtri  14655  comet  14678  bdxmet  14680  txmetcnp  14697  metcnpd  14699  cnmet  14709  ioo2bl  14730  mpomulcn  14745  fsumcncntop  14746  elcncf  14752  mulc1cncf  14768  cncfco  14770  cncfcncntop  14772  cncfmptc  14775  cncfmptid  14776  addccncf  14779  cdivcncfap  14783  negcncf  14784  mulcncflem  14786  limccnp2cntop  14856  reldvg  14858  dvfvalap  14860  eldvap  14861  dvconst  14873  dvconstre  14875  dvconstss  14877  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  dvexp  14890  dvrecap  14892  dvmptid  14895  dvmptc  14896  dveflem  14905  dvef  14906  elplyd  14920  ply1termlem  14921  plyaddlem1  14926  plymullem1  14927  plyadd  14930  plymul  14931  plycolemc  14936  plyco  14937  plycjlemc  14938  plycj  14939  plyrecj  14941  dvply1  14943  sinperlem  14984  sinmpi  14991  cosmpi  14992  sinppi  14993  cosppi  14994  efimpi  14995  sinhalfpip  14996  sinhalfpim  14997  coshalfpip  14998  coshalfpim  14999  ptolemy  15000  tangtx  15014  logdivlti  15057  rpcxpadd  15081  rpmulcxp  15085  rplogbchbase  15123  rprelogbmul  15128  binom4  15152  wilthlem1  15153  lgsval  15161  lgsfvalg  15162  lgsval2lem  15167  lgsval4a  15179  lgsneg  15181  lgsdilem  15184  lgsdirprm  15191  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  gausslemma2dlem4  15221  gausslemma2dlem6  15224  lgseisenlem2  15228  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem1  15238  lgsquad2lem2  15239  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2sqlem2  15272  2sqlem3  15274  2sqlem4  15275  2sqlem8  15280  cvgcmp2nlemabs  15592  trilpolemclim  15596  trilpolemcl  15597  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  trilpo  15603  redcwlpo  15615  nconstwlpolemgt0  15624  nconstwlpo  15626  neapmkv  15628