Theorem oveq12d 6093

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	⊢ (𝜑 → 𝐴 = 𝐵)
oveq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
oveq12d	⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveq12d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq12d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
3		oveq12 6084	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   = wceq 1402  (class class class)co 6075

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078

This theorem is referenced by:  oveq123d  6096  ovmpodxf  6204  ovmpodf  6210  caovdig  6254  caovdir2d  6256  caovdirg  6257  caovdilemd  6271  caovlem2d  6272  offval  6300  ofvalg  6302  offval2  6308  ofco  6311  caofinvl  6318  offres  6358  nnmsucr  6751  nndir  6753  ecovdi  6910  ecovidi  6911  dfplpq2  7711  dfmpq2  7712  addcmpblnq  7724  mulpipqqs  7730  addassnqg  7739  distrnqg  7744  ltaddnq  7764  halfnqq  7767  enq0tr  7791  addcmpblnq0  7800  addnq0mo  7804  addnnnq0  7806  nqnq0a  7811  distrnq0  7816  addassnq0  7819  distnq0r  7820  nq02m  7822  ltexpri  7970  cauappcvgprlemm  8002  cauappcvgprlemloc  8009  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem1  8016  cauappcvgprlem2  8017  cauappcvgprlemlim  8018  cauappcvgpr  8019  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemm  8025  caucvgprlemloc  8032  caucvgprlemcl  8033  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprlem2  8037  caucvgpr  8039  caucvgprprlemelu  8043  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemmu  8052  caucvgprprlemopu  8056  caucvgprprlemloc  8060  caucvgprprlemclphr  8062  caucvgprprlemexbt  8063  caucvgprprlem2  8067  mulcmpblnrlemg  8097  mulsrmo  8101  mulsrpr  8103  mulcomsrg  8114  distrsrg  8116  recexgt0sr  8130  mulgt0sr  8135  mulextsr1lem  8137  caucvgsrlemgt1  8152  caucvgsr  8159  addcnsr  8191  mulcnsr  8192  recidpirqlemcalc  8214  axaddcl  8221  axmulcl  8223  axmulcom  8228  axmulass  8230  axdistr  8231  axcaucvglemcau  8255  axcaucvglemres  8256  adddir  8307  muladd11  8449  1p1times  8450  muladd11r  8472  pnpcan2  8556  muladd  8701  subdir  8703  mulsub  8718  mulreim  8922  apadd1  8926  mulext1  8930  recextlem1  8969  muleqadd  8988  divdirap  9017  divadddivap  9047  conjmulap  9049  divcanap5rd  9138  subrecap  9159  xp1d2m1eqxm1d2  9537  div4p1lem1div2  9538  cnref1o  10030  xnegid  10240  xposdif  10263  xleaddadd  10268  icoshftf1o  10372  lincmb01cmp  10384  iccf1o  10386  fz01en  10437  fzrev3  10472  fzrevral2  10491  fzrevral3  10492  fzshftral  10493  fzoaddel2  10586  fzosubel  10590  fzosubel2  10591  fzocatel  10595  modqsubdir  10808  addmodlteq  10813  frecuzrdgsuc  10829  frecfzen2  10842  iseqovex  10873  seqvalcd  10876  seq3caopr3  10906  seqcaopr3g  10907  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seq3f1olemqsum  10928  seqf1oglem2  10935  seq3id3  10939  seqfeq3  10944  seq3distr  10947  ser3le  10952  mulexp  10993  mulexpzap  10994  expaddzap  10998  expubnd  11011  subsq  11061  binom2  11066  binom21  11067  binom2sub  11068  binom2sub1  11069  binom3  11072  sqoddm1div8  11109  mulsubdivbinom2ap  11127  nn0opthlem1d  11136  nn0opthd  11138  facp1  11146  facubnd  11161  bcval  11165  bcn1  11174  bcm1k  11176  bcp1n  11177  bcp1nk  11178  bcval5  11179  bcn2  11180  bcpasc  11182  bcm1n  11185  hashun  11223  hashfz  11240  hashfibclem  11260  hashfibc  11261  hashf1lem2  11264  hashf1  11265  hashtpgim  11275  ccatlid  11352  ccatass  11354  ccat1st1st  11387  swrdval  11398  swrdspsleq  11417  ccatswrd  11420  pfxval  11424  addlenpfx  11441  ccatpfx  11451  ccatopth  11466  pfxccatin12lem1  11478  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12  11483  swrdccat  11485  swrdccat3blem  11489  swrdccatin2d  11494  pfxccatin12d  11495  cats1lend  11517  cats2catd  11519  s2eqd  11520  s3eqd  11521  s4eqd  11522  s5eqd  11523  s6eqd  11524  s7eqd  11525  s8eqd  11526  crre  11600  replim  11602  remullem  11614  remul2  11616  immul2  11623  cjcj  11626  cjadd  11627  ipcnval  11629  cjmulval  11631  cjneg  11633  imval2  11637  cjreim  11647  cvg1nlemcau  11728  cvg1nlemres  11729  resqrexlemp1rp  11750  resqrexlemfp1  11753  resqrexlemcalc1  11758  resqrexlemcalc2  11759  resqrex  11770  sqabsadd  11799  sqabssub  11800  absreimsq  11811  recan  11853  amgm2  11862  maxabslemab  11950  maxabslemval  11952  max0addsup  11963  minabs  11980  bdtrilem  11983  bdtri  11984  xrmaxadd  12005  xrminadd  12019  xrbdtri  12020  subcn2  12055  reccn2ap  12057  climle  12078  climcvg1nlem  12093  serf0  12096  fsumadd  12151  fsumsplit  12152  sumpr  12158  sumtp  12159  isumadd  12176  sumsplitdc  12177  fsum2dlemstep  12179  fsumshftm  12190  fisumrev2  12191  fsumconst  12199  modfsummodlemstep  12202  telfsumo  12211  fsumparts  12215  binomlem  12228  binom  12229  binom1dif  12232  bcxmaslem1  12233  isumsplit  12236  isumnn0nn  12238  arisum  12243  arisum2  12244  trireciplem  12245  trirecip  12246  geosergap  12251  geo2sum  12259  geo2sum2  12260  cvgratnnlemsumlt  12273  mertenslemi1  12280  mertensabs  12282  fprodmul  12336  fprodsplitdc  12341  fprodabs  12361  fprod2dlemstep  12367  fproddivapf  12376  eftabs  12401  eftvalcn  12402  efcllemp  12403  ege2le3  12416  efcj  12418  efaddlem  12419  efsep  12436  ef4p  12439  efgt1p2  12440  efgt1p  12441  sinval  12447  cosval  12448  tanvalap  12453  tanval2ap  12458  tanval3ap  12459  efi4p  12462  sinneg  12471  cosneg  12472  tannegap  12473  efival  12477  efmival  12478  sinadd  12481  cosadd  12482  tanaddaplem  12483  tanaddap  12484  sinsub  12485  cossub  12486  addsin  12487  subsin  12488  sinmul  12489  cosmul  12490  addcos  12491  subcos  12492  sincossq  12493  cos2t  12495  sin01bnd  12502  cos01bnd  12503  efieq1re  12517  demoivreALT  12519  dvds2ln  12569  odd2np1lem  12617  bitsinv1lem  12706  gcdaddm  12739  bezoutlemnewy  12751  dfgcd3  12765  dvdsgcd  12767  mulgcd  12771  mulgcdr  12773  gcddiv  12774  sqgcd  12784  lcmgcdlem  12833  lcmgcd  12834  qredeu  12853  divgcdcoprm0  12857  cncongr1  12859  oddpwdclemdc  12929  sqrt2irraplemnn  12935  qnumdenbi  12948  zgcdsq  12957  hashdvds  12977  phiprmpw  12978  phimullem  12981  eulerthlema  12986  prmdiv  12991  modprm0  13011  coprimeprodsq  13014  pythagtriplem1  13022  pythagtriplem12  13032  pythagtriplem14  13034  pythagtriplem15  13035  pythagtriplem16  13036  pythagtriplem17  13037  pythagtriplem19  13039  pcval  13053  pcmul  13058  pcdiv  13059  pcqmul  13060  pcid  13081  pcaddlem  13096  pcmpt  13100  pcmpt2  13101  pcmptdvds  13102  pcbc  13108  4sqlem4  13149  mul4sqlem  13150  mul4sq  13151  4sqlem11  13158  4sqlem12  13159  4sqlem15  13162  4sqlem17  13164  ballotfilemfval  13207  ballotfilemfp1  13209  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemfmpn  13212  ballotfilemgval  13245  ballotfilemgun  13246  ballotfilemfrc  13248  ballotfilemfrceq  13250  ennnfonelemp1  13275  nninfdclemp1  13319  ressvalsets  13395  topnvalg  13582  topnpropgd  13584  qusval  13621  qusex  13623  qusaddvallemg  13631  imasmnd2  13736  ismhm  13745  mhmf1o  13754  0mhm  13770  mhmco  13774  mhmeql  13776  isgrpid2  13822  grpnpcan  13874  imasgrp2  13890  mhmmnd  13896  mulgnndir  13931  mulgdir  13934  isnsg3  13987  isghm  14023  ghmnsgima  14048  ghmf1o  14055  conjghm  14056  qusghm  14062  ablsub4  14094  ghmcmn  14108  invghm  14110  gzsumconst  14120  gzsumgsum  14132  gsump1  14134  gsumzfi  14135  gsummptfidmadd  14138  gsumconstcmn  14143  prdsex  14149  prdsval  14150  xpsval  14178  pwsval  14181  mgpvalg  14197  mgptopng  14203  mgpress  14205  rngdi  14214  rngdir  14215  rngpropd  14229  imasrng  14230  srglmhm  14271  srgrmhm  14272  ringo2times  14306  ringcom  14309  ringpropd  14316  ring1  14337  ringlghm  14339  ringrghm  14340  imasring  14342  opprvalg  14347  opprrng  14355  opprring  14357  invrfvald  14402  dvrvald  14414  dvrdir  14423  rdivmuldivd  14424  islmod  14600  lmodlema  14601  islmodd  14602  lmodcom  14642  lmodnegadd  14645  lmodprop2d  14657  rmodislmod  14660  lsssn0  14679  sraval  14746  qusrhm  14837  gsumfsum  14895  expghmap  14914  mulgghm2  14915  mulgrhm  14916  zlmval  14934  znval  14943  psrval  14973  mplvalcoe  15004  cnfval  15218  cnpfval  15219  ispsmet  15347  psmet0  15351  psmettri2  15352  psmetres2  15357  ismet  15368  isxmet  15369  xmettri2  15385  xmetres2  15403  xblss2  15429  xmstri2  15494  mstri2  15495  xmstri  15496  mstri  15497  xmstri3  15498  mstri3  15499  msrtri  15500  comet  15523  bdxmet  15525  txmetcnp  15542  metcnpd  15544  cnmet  15554  ioo2bl  15575  mpomulcn  15590  fsumcncntop  15591  elcncf  15597  mulc1cncf  15613  cncfco  15615  cncfcncntop  15617  cncfmptc  15620  cncfmptid  15621  addccncf  15624  cdivcncfap  15628  negcncf  15629  mulcncflem  15631  limccnp2cntop  15701  reldvg  15703  dvfvalap  15705  eldvap  15706  dvconst  15718  dvconstre  15720  dvconstss  15722  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  dvexp  15735  dvrecap  15737  dvmptid  15740  dvmptc  15741  dveflem  15750  dvef  15751  elplyd  15765  ply1termlem  15766  plyaddlem1  15771  plymullem1  15772  plyadd  15775  plymul  15776  plycoeid3  15781  plycolemc  15782  plyco  15783  plycjlemc  15784  plycj  15785  plyrecj  15787  dvply1  15789  dvply2g  15790  sinperlem  15832  sinmpi  15839  cosmpi  15840  sinppi  15841  cosppi  15842  efimpi  15843  sinhalfpip  15844  sinhalfpim  15845  coshalfpip  15846  coshalfpim  15847  ptolemy  15848  tangtx  15862  logdivlti  15905  rpcxpadd  15930  rpmulcxp  15934  rplogbchbase  15975  rprelogbmul  15980  binom4  16004  pellexlem2  16006  pellexlem3  16007  wilthlem1  16008  1sgmprm  16022  1sgm2ppw  16023  sgmmul  16024  mersenne  16025  perfect1  16026  perfectlem2  16028  perfect  16029  lgsval  16037  lgsfvalg  16038  lgsval2lem  16043  lgsval4a  16055  lgsneg  16057  lgsdilem  16060  lgsdirprm  16067  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  gausslemma2dlem4  16097  gausslemma2dlem6  16100  lgseisenlem2  16104  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad2lem1  16114  lgsquad2lem2  16115  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2sqlem2  16148  2sqlem3  16150  2sqlem4  16151  2sqlem8  16156  vtxdgfval  16443  vtxdgfifival  16446  vtxdgop  16447  vtxdgfi0e  16450  vtxdeqd  16451  vtxdfifiun  16452  vtxduspgrfvedgfi  16456  1loopgrvd2fi  16460  repiecele0  16980  repiecege0  16981  repiecef  16982  cvgcmp2nlemabs  16986  trilpolemclim  16990  trilpolemcl  16991  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  trilpo  16997  redcwlpo  17010  nconstwlpolemgt0  17019  nconstwlpo  17021  neapmkv  17023