Theorem oveq12d 6103

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 6094	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	syl2anc 415	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1402  (class class class)co 6085

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq123d  6106  ovmpodxf  6214  ovmpodf  6220  caovdig  6264  caovdir2d  6266  caovdirg  6267  caovdilemd  6281  caovlem2d  6282  offval  6310  ofvalg  6312  offval2  6318  ofco  6321  caofinvl  6328  offres  6368  nnmsucr  6761  nndir  6763  ecovdi  6920  ecovidi  6921  dfplpq2  7721  dfmpq2  7722  addcmpblnq  7734  mulpipqqs  7740  addassnqg  7749  distrnqg  7754  ltaddnq  7774  halfnqq  7777  enq0tr  7801  addcmpblnq0  7810  addnq0mo  7814  addnnnq0  7816  nqnq0a  7821  distrnq0  7826  addassnq0  7829  distnq0r  7830  nq02m  7832  ltexpri  7980  cauappcvgprlemm  8012  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlem2  8027  cauappcvgprlemlim  8028  cauappcvgpr  8029  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem2  8047  caucvgpr  8049  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemmu  8062  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexbt  8073  caucvgprprlem2  8077  mulcmpblnrlemg  8107  mulsrmo  8111  mulsrpr  8113  mulcomsrg  8124  distrsrg  8126  recexgt0sr  8140  mulgt0sr  8145  mulextsr1lem  8147  caucvgsrlemgt1  8162  caucvgsr  8169  addcnsr  8201  mulcnsr  8202  recidpirqlemcalc  8224  axaddcl  8231  axmulcl  8233  axmulcom  8238  axmulass  8240  axdistr  8241  axcaucvglemcau  8265  axcaucvglemres  8266  adddir  8317  muladd11  8460  1p1times  8461  muladd11r  8483  pnpcan2  8567  muladd  8712  subdir  8714  mulsub  8729  mulreim  8934  apadd1  8938  mulext1  8942  recextlem1  8981  muleqadd  9000  divdirap  9029  divadddivap  9059  conjmulap  9061  divcanap5rd  9150  subrecap  9171  xp1d2m1eqxm1d2  9562  div4p1lem1div2  9563  cnref1o  10061  xnegid  10271  xposdif  10294  xleaddadd  10299  icoshftf1o  10403  lincmb01cmp  10415  iccf1o  10417  fz01en  10469  fzrev3  10504  fzrevral2  10523  fzrevral3  10524  fzshftral  10525  fzoaddel2  10618  fzosubel  10622  fzosubel2  10623  fzocatel  10627  modqsubdir  10843  addmodlteq  10848  frecuzrdgsuc  10864  frecfzen2  10877  iseqovex  10908  seqvalcd  10911  seq3caopr3  10941  seqcaopr3g  10942  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seq3f1olemqsum  10963  seqf1oglem2  10970  seq3id3  10974  seqfeq3  10979  seq3distr  10982  ser3le  10987  mulexp  11028  mulexpzap  11029  expaddzap  11033  expubnd  11046  subsq  11096  binom2  11101  binom21  11102  binom2sub  11103  binom2sub1  11104  binom3  11107  sqoddm1div8  11144  mulsubdivbinom2ap  11163  nn0opthlem1d  11172  nn0opthd  11174  facp1  11182  facubnd  11197  bcval  11201  bcn1  11210  bcm1k  11212  bcp1n  11213  bcp1nk  11214  bcval5  11215  bcn2  11216  bcpasc  11218  bcm1n  11221  hashun  11259  hashfz  11276  hashfibclem  11296  hashfibc  11297  hashf1lem2  11300  hashf1  11301  hashtpgim  11311  ccatlid  11388  ccatass  11390  ccat1st1st  11423  swrdval  11434  swrdspsleq  11453  ccatswrd  11456  pfxval  11460  addlenpfx  11477  ccatpfx  11487  ccatopth  11502  pfxccatin12lem1  11514  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12  11519  swrdccat  11521  swrdccat3blem  11525  swrdccatin2d  11530  pfxccatin12d  11531  cats1lend  11553  cats2catd  11555  s2eqd  11556  s3eqd  11557  s4eqd  11558  s5eqd  11559  s6eqd  11560  s7eqd  11561  s8eqd  11562  crre  11636  replim  11638  remullem  11650  remul2  11652  immul2  11659  cjcj  11662  cjadd  11663  ipcnval  11665  cjmulval  11667  cjneg  11669  imval2  11673  cjreim  11683  cvg1nlemcau  11764  cvg1nlemres  11765  resqrexlemp1rp  11786  resqrexlemfp1  11789  resqrexlemcalc1  11794  resqrexlemcalc2  11795  resqrex  11806  sqabsadd  11835  sqabssub  11836  absreimsq  11847  recan  11890  amgm2  11899  maxabslemab  11987  maxabslemval  11989  max0addsup  12000  minabs  12017  bdtrilem  12021  bdtri  12022  xrmaxadd  12043  xrminadd  12057  xrbdtri  12058  subcn2  12093  reccn2ap  12095  climle  12116  climcvg1nlem  12131  serf0  12134  fsumadd  12189  fsumsplit  12190  sumpr  12196  sumtp  12197  isumadd  12214  sumsplitdc  12215  fsum2dlemstep  12217  fsumshftm  12228  fisumrev2  12229  fsumconst  12237  modfsummodlemstep  12240  telfsumo  12249  fsumparts  12253  binomlem  12266  binom  12267  binom1dif  12270  bcxmaslem1  12271  isumsplit  12274  isumnn0nn  12276  arisum  12281  arisum2  12282  trireciplem  12283  trirecip  12284  geosergap  12289  geo2sum  12297  geo2sum2  12298  cvgratnnlemsumlt  12311  mertenslemi1  12318  mertensabs  12320  fprodmul  12374  fprodsplitdc  12379  fprodabs  12399  fprod2dlemstep  12405  fproddivapf  12414  eftabs  12439  eftvalcn  12440  efcllemp  12441  ege2le3  12454  efcj  12456  efaddlem  12457  efsep  12474  ef4p  12477  efgt1p2  12478  efgt1p  12479  sinval  12485  cosval  12486  tanvalap  12491  tanval2ap  12496  tanval3ap  12497  efi4p  12500  sinneg  12509  cosneg  12510  tannegap  12511  efival  12515  efmival  12516  sinadd  12519  cosadd  12520  tanaddaplem  12521  tanaddap  12522  sinsub  12523  cossub  12524  addsin  12525  subsin  12526  sinmul  12527  cosmul  12528  addcos  12529  subcos  12530  sincossq  12531  cos2t  12533  sin01bnd  12540  cos01bnd  12541  efieq1re  12555  demoivreALT  12557  dvds2ln  12607  odd2np1lem  12655  bitsinv1lem  12744  gcdaddm  12777  bezoutlemnewy  12789  dfgcd3  12803  dvdsgcd  12805  mulgcd  12809  mulgcdr  12811  gcddiv  12812  sqgcd  12822  lcmgcdlem  12871  lcmgcd  12872  qredeu  12891  divgcdcoprm0  12895  cncongr1  12897  nnmaxpwlemparts  12968  sqrt2irraplemnn  12975  qnumdenbi  12988  zgcdsq  12997  hashdvds  13019  phiprmpw  13020  phimullem  13023  eulerthlema  13028  prmdiv  13033  modprm0  13053  coprimeprodsq  13056  pythagtriplem1  13064  pythagtriplem12  13074  pythagtriplem14  13076  pythagtriplem15  13077  pythagtriplem16  13078  pythagtriplem17  13079  pythagtriplem19  13081  pcval  13095  pcmul  13100  pcdiv  13101  pcqmul  13102  pcid  13123  pcaddlem  13138  pcmpt  13142  pcmpt2  13143  pcmptdvds  13144  pcbc  13150  4sqlem4  13191  mul4sqlem  13192  mul4sq  13193  4sqlem11  13200  4sqlem12  13201  4sqlem15  13204  4sqlem17  13206  ballotfilemfval  13278  ballotfilemfp1  13280  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemfmpn  13283  ballotfilemgval  13316  ballotfilemgun  13317  ballotfilemfrc  13319  ballotfilemfrceq  13321  ennnfonelemp1  13346  nninfdclemp1  13390  ressvalsets  13467  topnvalg  13654  topnpropgd  13656  qusval  13693  qusex  13695  qusaddvallemg  13703  imasmnd2  13808  ismhm  13817  mhmf1o  13826  0mhm  13842  mhmco  13846  mhmeql  13848  isgrpid2  13894  grpnpcan  13946  imasgrp2  13962  mhmmnd  13968  mulgnndir  14003  mulgdir  14006  isnsg3  14059  isghm  14095  ghmnsgima  14120  ghmf1o  14127  conjghm  14128  qusghm  14134  ablsub4  14166  ghmcmn  14180  invghm  14182  gzsumconst  14192  gzsumgsum  14204  gsump1  14206  gsumzfi  14207  gsummptfidmadd  14210  gsumconstcmn  14215  prdsex  14221  prdsval  14222  xpsval  14250  pwsval  14253  mgpvalg  14269  mgptopng  14277  mgpress  14279  rngdi  14288  rngdir  14289  rngpropd  14303  imasrng  14304  srglmhm  14346  srgrmhm  14347  ringo2times  14382  ringcom  14385  ringpropd  14392  ring1  14413  ringlghm  14415  ringrghm  14416  imasring  14418  opprvalg  14423  opprrng  14431  opprring  14433  invrfvald  14478  dvrvald  14490  dvrdir  14499  rdivmuldivd  14500  islmod  14676  lmodlema  14677  islmodd  14678  lmodcom  14719  lmodnegadd  14722  lmodprop2d  14734  rmodislmod  14737  lsssn0  14756  sraval  14823  qusrhm  14914  gsumfsum  14972  expghmap  14991  mulgghm2  14992  mulgrhm  14993  zlmval  15011  znval  15020  asclghm  15074  assamulgscmlem1  15090  assamulgscm  15092  psrval  15099  mplvalcoe  15130  cnfval  15344  cnpfval  15345  ispsmet  15473  psmet0  15477  psmettri2  15478  psmetres2  15483  ismet  15494  isxmet  15495  xmettri2  15511  xmetres2  15529  xblss2  15555  xmstri2  15620  mstri2  15621  xmstri  15622  mstri  15623  xmstri3  15624  mstri3  15625  msrtri  15626  comet  15649  bdxmet  15651  txmetcnp  15668  metcnpd  15670  cnmet  15680  ioo2bl  15701  mpomulcn  15716  fsumcncntop  15717  elcncf  15723  mulc1cncf  15739  cncfco  15741  cncfcncntop  15743  cncfmptc  15746  cncfmptid  15747  addccncf  15750  cdivcncfap  15754  negcncf  15755  mulcncflem  15757  limccnp2cntop  15827  reldvg  15829  dvfvalap  15831  eldvap  15832  dvconst  15844  dvconstre  15846  dvconstss  15848  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvexp  15861  dvrecap  15863  dvmptid  15866  dvmptc  15867  dveflem  15876  dvef  15877  elplyd  15891  ply1termlem  15892  plyaddlem1  15897  plymullem1  15898  plyadd  15901  plymul  15902  plycoeid3  15907  plycolemc  15908  plyco  15909  plycjlemc  15910  plycj  15911  plyrecj  15913  dvply1  15915  dvply2g  15916  sinperlem  15959  sinmpi  15966  cosmpi  15967  sinppi  15968  cosppi  15969  efimpi  15970  sinhalfpip  15971  sinhalfpim  15972  coshalfpip  15973  coshalfpim  15974  ptolemy  15975  tangtx  15989  logdivlti  16033  rpcxpadd  16060  rpmulcxp  16064  rplogbchbase  16105  rprelogbmul  16110  binom4  16138  log2tlbndlog2  16139  log2ublem2  16141  birthdaylem2  16145  pellexlem2  16149  pellexlem3  16150  wilthlem1  16151  ppidif  16175  1sgmprm  16189  1sgm2ppw  16190  sgmmul  16191  ppiqub  16194  mersenne  16195  perfect1  16196  perfectlem2  16198  perfect  16199  bcmono  16202  bcp1ctr  16204  bclbnd  16205  bposlem1  16209  bposlem2  16210  bposlem5  16213  lgsval  16221  lgsfvalg  16222  lgsval2lem  16227  lgsval4a  16239  lgsneg  16241  lgsdilem  16244  lgsdirprm  16251  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  gausslemma2dlem4  16281  gausslemma2dlem6  16284  lgseisenlem2  16288  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad2lem1  16298  lgsquad2lem2  16299  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2sqlem2  16332  2sqlem3  16334  2sqlem4  16335  2sqlem8  16340  vtxdgfval  16627  vtxdgfifival  16630  vtxdgop  16631  vtxdgfi0e  16634  vtxdeqd  16635  vtxdfifiun  16636  vtxduspgrfvedgfi  16640  1loopgrvd2fi  16644  repiecele0  17173  repiecege0  17174  repiecef  17175  cvgcmp2nlemabs  17179  trilpolemclim  17183  trilpolemcl  17184  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  trilpo  17190  redcwlpo  17203  nconstwlpolemgt0  17212  nconstwlpo  17214  neapmkv  17216