Theorem oveq12d 5792

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

Syntax hints:   -> wi 4   = wceq 1331  (class class class)co 5774

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777

This theorem is referenced by:  oveq123d  5795  ovmpodxf  5896  ovmpodf  5902  caovdig  5945  caovdir2d  5947  caovdirg  5948  caovdilemd  5962  caovlem2d  5963  offval  5989  ofvalg  5991  offval2  5997  ofco  6000  caofinvl  6004  offres  6033  nnmsucr  6384  nndir  6386  ecovdi  6540  ecovidi  6541  dfplpq2  7162  dfmpq2  7163  addcmpblnq  7175  mulpipqqs  7181  addassnqg  7190  distrnqg  7195  ltaddnq  7215  halfnqq  7218  enq0tr  7242  addcmpblnq0  7251  addnq0mo  7255  addnnnq0  7257  nqnq0a  7262  distrnq0  7267  addassnq0  7270  distnq0r  7271  nq02m  7273  ltexpri  7421  cauappcvgprlemm  7453  cauappcvgprlemloc  7460  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem1  7467  cauappcvgprlem2  7468  cauappcvgprlemlim  7469  cauappcvgpr  7470  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemm  7476  caucvgprlemloc  7483  caucvgprlemcl  7484  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlem2  7488  caucvgpr  7490  caucvgprprlemelu  7494  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemmu  7503  caucvgprprlemopu  7507  caucvgprprlemloc  7511  caucvgprprlemclphr  7513  caucvgprprlemexbt  7514  caucvgprprlem2  7518  mulcmpblnrlemg  7548  mulsrmo  7552  mulsrpr  7554  mulcomsrg  7565  distrsrg  7567  recexgt0sr  7581  mulgt0sr  7586  mulextsr1lem  7588  caucvgsrlemgt1  7603  caucvgsr  7610  addcnsr  7642  mulcnsr  7643  recidpirqlemcalc  7665  axaddcl  7672  axmulcl  7674  axmulcom  7679  axmulass  7681  axdistr  7682  axcaucvglemcau  7706  axcaucvglemres  7707  adddir  7757  muladd11  7895  1p1times  7896  muladd11r  7918  pnpcan2  8002  muladd  8146  subdir  8148  mulsub  8163  mulreim  8366  apadd1  8370  mulext1  8374  recextlem1  8412  muleqadd  8429  divdirap  8457  divadddivap  8487  conjmulap  8489  divcanap5rd  8578  subrecap  8598  xp1d2m1eqxm1d2  8972  div4p1lem1div2  8973  cnref1o  9440  xnegid  9642  xposdif  9665  xleaddadd  9670  icoshftf1o  9774  lincmb01cmp  9786  iccf1o  9787  fz01en  9833  fzrev3  9867  fzrevral2  9886  fzrevral3  9887  fzshftral  9888  fzoaddel2  9970  fzosubel  9971  fzosubel2  9972  fzocatel  9976  modqsubdir  10166  addmodlteq  10171  frecuzrdgsuc  10187  frecfzen2  10200  iseqovex  10229  seqvalcd  10232  seq3caopr3  10254  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  seq3id3  10280  seqfeq3  10285  seq3distr  10286  ser3le  10291  mulexp  10332  mulexpzap  10333  expaddzap  10337  expubnd  10350  subsq  10399  binom2  10403  binom21  10404  binom2sub  10405  binom2sub1  10406  binom3  10409  sqoddm1div8  10444  nn0opthlem1d  10466  nn0opthd  10468  facp1  10476  facubnd  10491  bcval  10495  bcn1  10504  bcm1k  10506  bcp1n  10507  bcp1nk  10508  bcval5  10509  bcn2  10510  bcpasc  10512  hashun  10551  hashfz  10567  crre  10629  replim  10631  remullem  10643  remul2  10645  immul2  10652  cjcj  10655  cjadd  10656  ipcnval  10658  cjmulval  10660  cjneg  10662  imval2  10666  cjreim  10675  cvg1nlemcau  10756  cvg1nlemres  10757  resqrexlemp1rp  10778  resqrexlemfp1  10781  resqrexlemcalc1  10786  resqrexlemcalc2  10787  resqrex  10798  sqabsadd  10827  sqabssub  10828  absreimsq  10839  recan  10881  amgm2  10890  maxabslemab  10978  maxabslemval  10980  max0addsup  10991  minabs  11007  bdtrilem  11010  bdtri  11011  xrmaxadd  11030  xrminadd  11044  xrbdtri  11045  subcn2  11080  reccn2ap  11082  climle  11103  climcvg1nlem  11118  serf0  11121  fsumadd  11175  fsumsplit  11176  sumpr  11182  sumtp  11183  isumadd  11200  sumsplitdc  11201  fsum2dlemstep  11203  fsumshftm  11214  fisumrev2  11215  fsumconst  11223  modfsummodlemstep  11226  telfsumo  11235  fsumparts  11239  binomlem  11252  binom  11253  binom1dif  11256  bcxmaslem1  11257  isumsplit  11260  isumnn0nn  11262  arisum  11267  arisum2  11268  trireciplem  11269  trirecip  11270  geosergap  11275  geo2sum  11283  geo2sum2  11284  cvgratnnlemsumlt  11297  mertenslemi1  11304  mertensabs  11306  eftabs  11362  eftvalcn  11363  efcllemp  11364  ege2le3  11377  efcj  11379  efaddlem  11380  efsep  11397  ef4p  11400  efgt1p2  11401  efgt1p  11402  sinval  11409  cosval  11410  tanvalap  11415  tanval2ap  11420  tanval3ap  11421  efi4p  11424  sinneg  11433  cosneg  11434  tannegap  11435  efival  11439  efmival  11440  sinadd  11443  cosadd  11444  tanaddaplem  11445  tanaddap  11446  sinsub  11447  cossub  11448  addsin  11449  subsin  11450  sinmul  11451  cosmul  11452  addcos  11453  subcos  11454  sincossq  11455  cos2t  11457  sin01bnd  11464  cos01bnd  11465  efieq1re  11478  demoivreALT  11480  dvds2ln  11526  odd2np1lem  11569  gcdaddm  11672  bezoutlemnewy  11684  dfgcd3  11698  dvdsgcd  11700  mulgcd  11704  mulgcdr  11706  gcddiv  11707  sqgcd  11717  lcmgcdlem  11758  lcmgcd  11759  qredeu  11778  divgcdcoprm0  11782  cncongr1  11784  oddpwdclemdc  11851  sqrt2irraplemnn  11857  qnumdenbi  11870  zgcdsq  11879  hashdvds  11897  phiprmpw  11898  phimullem  11901  ennnfonelemp1  11919  ressid2  12018  ressval2  12019  topnvalg  12132  topnpropgd  12134  cnfval  12363  cnpfval  12364  ispsmet  12492  psmet0  12496  psmettri2  12497  psmetres2  12502  ismet  12513  isxmet  12514  xmettri2  12530  xmetres2  12548  xblss2  12574  xmstri2  12639  mstri2  12640  xmstri  12641  mstri  12642  xmstri3  12643  mstri3  12644  msrtri  12645  comet  12668  bdxmet  12670  txmetcnp  12687  metcnpd  12689  cnmet  12699  ioo2bl  12712  fsumcncntop  12725  elcncf  12729  mulc1cncf  12745  cncfco  12747  cncfcncntop  12749  cncfmptc  12751  cncfmptid  12752  addccncf  12755  cdivcncfap  12756  negcncf  12757  mulcncflem  12759  limccnp2cntop  12815  reldvg  12817  dvfvalap  12819  eldvap  12820  dvconst  12830  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  dvcjbr  12841  dvexp  12844  dvrecap  12846  dveflem  12855  dvef  12856  sinperlem  12889  sinmpi  12896  cosmpi  12897  sinppi  12898  cosppi  12899  efimpi  12900  sinhalfpip  12901  sinhalfpim  12902  coshalfpip  12903  coshalfpim  12904  ptolemy  12905  tangtx  12919  cvgcmp2nlemabs  13227  trilpolemclim  13229  trilpolemcl  13230  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234  trilpo  13236