Theorem oveq12d 5975

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

Syntax hints:   → wi 4   = wceq 1373  (class class class)co 5957

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rex 2491  df-v 2775  df-un 3174  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-iota 5241  df-fv 5288  df-ov 5960

This theorem is referenced by:  oveq123d  5978  ovmpodxf  6084  ovmpodf  6090  caovdig  6134  caovdir2d  6136  caovdirg  6137  caovdilemd  6151  caovlem2d  6152  offval  6179  ofvalg  6181  offval2  6187  ofco  6190  caofinvl  6197  offres  6233  nnmsucr  6587  nndir  6589  ecovdi  6746  ecovidi  6747  dfplpq2  7487  dfmpq2  7488  addcmpblnq  7500  mulpipqqs  7506  addassnqg  7515  distrnqg  7520  ltaddnq  7540  halfnqq  7543  enq0tr  7567  addcmpblnq0  7576  addnq0mo  7580  addnnnq0  7582  nqnq0a  7587  distrnq0  7592  addassnq0  7595  distnq0r  7596  nq02m  7598  ltexpri  7746  cauappcvgprlemm  7778  cauappcvgprlemloc  7785  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  cauappcvgprlem1  7792  cauappcvgprlem2  7793  cauappcvgprlemlim  7794  cauappcvgpr  7795  caucvgprlemnkj  7799  caucvgprlemnbj  7800  caucvgprlemm  7801  caucvgprlemloc  7808  caucvgprlemcl  7809  caucvgprlemladdfu  7810  caucvgprlemladdrl  7811  caucvgprlem2  7813  caucvgpr  7815  caucvgprprlemelu  7819  caucvgprprlemcbv  7820  caucvgprprlemval  7821  caucvgprprlemmu  7828  caucvgprprlemopu  7832  caucvgprprlemloc  7836  caucvgprprlemclphr  7838  caucvgprprlemexbt  7839  caucvgprprlem2  7843  mulcmpblnrlemg  7873  mulsrmo  7877  mulsrpr  7879  mulcomsrg  7890  distrsrg  7892  recexgt0sr  7906  mulgt0sr  7911  mulextsr1lem  7913  caucvgsrlemgt1  7928  caucvgsr  7935  addcnsr  7967  mulcnsr  7968  recidpirqlemcalc  7990  axaddcl  7997  axmulcl  7999  axmulcom  8004  axmulass  8006  axdistr  8007  axcaucvglemcau  8031  axcaucvglemres  8032  adddir  8083  muladd11  8225  1p1times  8226  muladd11r  8248  pnpcan2  8332  muladd  8476  subdir  8478  mulsub  8493  mulreim  8697  apadd1  8701  mulext1  8705  recextlem1  8744  muleqadd  8761  divdirap  8790  divadddivap  8820  conjmulap  8822  divcanap5rd  8911  subrecap  8932  xp1d2m1eqxm1d2  9310  div4p1lem1div2  9311  cnref1o  9792  xnegid  10001  xposdif  10024  xleaddadd  10029  icoshftf1o  10133  lincmb01cmp  10145  iccf1o  10146  fz01en  10195  fzrev3  10229  fzrevral2  10248  fzrevral3  10249  fzshftral  10250  fzoaddel2  10341  fzosubel  10345  fzosubel2  10346  fzocatel  10350  modqsubdir  10560  addmodlteq  10565  frecuzrdgsuc  10581  frecfzen2  10594  iseqovex  10625  seqvalcd  10628  seq3caopr3  10658  seqcaopr3g  10659  seq3f1olemqsumkj  10678  seq3f1olemqsumk  10679  seq3f1olemqsum  10680  seqf1oglem2  10687  seq3id3  10691  seqfeq3  10696  seq3distr  10699  ser3le  10704  mulexp  10745  mulexpzap  10746  expaddzap  10750  expubnd  10763  subsq  10813  binom2  10818  binom21  10819  binom2sub  10820  binom2sub1  10821  binom3  10824  sqoddm1div8  10860  mulsubdivbinom2ap  10878  nn0opthlem1d  10887  nn0opthd  10889  facp1  10897  facubnd  10912  bcval  10916  bcn1  10925  bcm1k  10927  bcp1n  10928  bcp1nk  10929  bcval5  10930  bcn2  10931  bcpasc  10933  hashun  10972  hashfz  10988  ccatlid  11085  ccatass  11087  ccat1st1st  11116  swrdval  11124  swrdspsleq  11143  ccatswrd  11146  pfxval  11150  addlenpfx  11167  ccatpfx  11177  ccatopth  11192  crre  11243  replim  11245  remullem  11257  remul2  11259  immul2  11266  cjcj  11269  cjadd  11270  ipcnval  11272  cjmulval  11274  cjneg  11276  imval2  11280  cjreim  11289  cvg1nlemcau  11370  cvg1nlemres  11371  resqrexlemp1rp  11392  resqrexlemfp1  11395  resqrexlemcalc1  11400  resqrexlemcalc2  11401  resqrex  11412  sqabsadd  11441  sqabssub  11442  absreimsq  11453  recan  11495  amgm2  11504  maxabslemab  11592  maxabslemval  11594  max0addsup  11605  minabs  11622  bdtrilem  11625  bdtri  11626  xrmaxadd  11647  xrminadd  11661  xrbdtri  11662  subcn2  11697  reccn2ap  11699  climle  11720  climcvg1nlem  11735  serf0  11738  fsumadd  11792  fsumsplit  11793  sumpr  11799  sumtp  11800  isumadd  11817  sumsplitdc  11818  fsum2dlemstep  11820  fsumshftm  11831  fisumrev2  11832  fsumconst  11840  modfsummodlemstep  11843  telfsumo  11852  fsumparts  11856  binomlem  11869  binom  11870  binom1dif  11873  bcxmaslem1  11874  isumsplit  11877  isumnn0nn  11879  arisum  11884  arisum2  11885  trireciplem  11886  trirecip  11887  geosergap  11892  geo2sum  11900  geo2sum2  11901  cvgratnnlemsumlt  11914  mertenslemi1  11921  mertensabs  11923  fprodmul  11977  fprodsplitdc  11982  fprodabs  12002  fprod2dlemstep  12008  fproddivapf  12017  eftabs  12042  eftvalcn  12043  efcllemp  12044  ege2le3  12057  efcj  12059  efaddlem  12060  efsep  12077  ef4p  12080  efgt1p2  12081  efgt1p  12082  sinval  12088  cosval  12089  tanvalap  12094  tanval2ap  12099  tanval3ap  12100  efi4p  12103  sinneg  12112  cosneg  12113  tannegap  12114  efival  12118  efmival  12119  sinadd  12122  cosadd  12123  tanaddaplem  12124  tanaddap  12125  sinsub  12126  cossub  12127  addsin  12128  subsin  12129  sinmul  12130  cosmul  12131  addcos  12132  subcos  12133  sincossq  12134  cos2t  12136  sin01bnd  12143  cos01bnd  12144  efieq1re  12158  demoivreALT  12160  dvds2ln  12210  odd2np1lem  12258  bitsinv1lem  12347  gcdaddm  12380  bezoutlemnewy  12392  dfgcd3  12406  dvdsgcd  12408  mulgcd  12412  mulgcdr  12414  gcddiv  12415  sqgcd  12425  lcmgcdlem  12474  lcmgcd  12475  qredeu  12494  divgcdcoprm0  12498  cncongr1  12500  oddpwdclemdc  12570  sqrt2irraplemnn  12576  qnumdenbi  12589  zgcdsq  12598  hashdvds  12618  phiprmpw  12619  phimullem  12622  eulerthlema  12627  prmdiv  12632  modprm0  12652  coprimeprodsq  12655  pythagtriplem1  12663  pythagtriplem12  12673  pythagtriplem14  12675  pythagtriplem15  12676  pythagtriplem16  12677  pythagtriplem17  12678  pythagtriplem19  12680  pcval  12694  pcmul  12699  pcdiv  12700  pcqmul  12701  pcid  12722  pcaddlem  12737  pcmpt  12741  pcmpt2  12742  pcmptdvds  12743  pcbc  12749  4sqlem4  12790  mul4sqlem  12791  mul4sq  12792  4sqlem11  12799  4sqlem12  12800  4sqlem15  12803  4sqlem17  12805  ennnfonelemp1  12852  nninfdclemp1  12896  ressvalsets  12971  topnvalg  13158  topnpropgd  13160  prdsex  13176  prdsval  13180  pwsval  13198  qusval  13230  qusex  13232  qusaddvallemg  13240  xpsval  13259  gsumprval  13306  imasmnd2  13359  ismhm  13368  mhmf1o  13377  0mhm  13393  mhmco  13397  mhmeql  13399  gsumfzz  13402  isgrpid2  13447  grpnpcan  13499  imasgrp2  13521  mhmmnd  13527  mulgnndir  13562  mulgdir  13565  isnsg3  13618  isghm  13654  ghmnsgima  13679  ghmf1o  13686  conjghm  13687  qusghm  13693  ablsub4  13724  ghmcmn  13738  invghm  13740  gsumfzmptfidmadd  13750  gsumfzconst  13752  mgpvalg  13760  mgptopng  13766  mgpress  13768  rngdi  13777  rngdir  13778  rngpropd  13792  imasrng  13793  srglmhm  13830  srgrmhm  13831  ringo2times  13865  ringcom  13868  ringpropd  13875  ring1  13896  ringlghm  13898  ringrghm  13899  imasring  13901  opprvalg  13906  opprrng  13914  opprring  13916  invrfvald  13959  dvrvald  13971  dvrdir  13980  rdivmuldivd  13981  islmod  14128  lmodlema  14129  islmodd  14130  lmodcom  14170  lmodnegadd  14173  lmodprop2d  14185  rmodislmod  14188  lsssn0  14207  sraval  14274  qusrhm  14365  gsumfzfsumlemm  14424  expghmap  14444  mulgghm2  14445  mulgrhm  14446  zlmval  14464  znval  14473  psrval  14503  mplvalcoe  14527  cnfval  14741  cnpfval  14742  ispsmet  14870  psmet0  14874  psmettri2  14875  psmetres2  14880  ismet  14891  isxmet  14892  xmettri2  14908  xmetres2  14926  xblss2  14952  xmstri2  15017  mstri2  15018  xmstri  15019  mstri  15020  xmstri3  15021  mstri3  15022  msrtri  15023  comet  15046  bdxmet  15048  txmetcnp  15065  metcnpd  15067  cnmet  15077  ioo2bl  15098  mpomulcn  15113  fsumcncntop  15114  elcncf  15120  mulc1cncf  15136  cncfco  15138  cncfcncntop  15140  cncfmptc  15143  cncfmptid  15144  addccncf  15147  cdivcncfap  15151  negcncf  15152  mulcncflem  15154  limccnp2cntop  15224  reldvg  15226  dvfvalap  15228  eldvap  15229  dvconst  15241  dvconstre  15243  dvconstss  15245  dvaddxxbr  15248  dvmulxxbr  15249  dvcoapbr  15254  dvcjbr  15255  dvexp  15258  dvrecap  15260  dvmptid  15263  dvmptc  15264  dveflem  15273  dvef  15274  elplyd  15288  ply1termlem  15289  plyaddlem1  15294  plymullem1  15295  plyadd  15298  plymul  15299  plycoeid3  15304  plycolemc  15305  plyco  15306  plycjlemc  15307  plycj  15308  plyrecj  15310  dvply1  15312  dvply2g  15313  sinperlem  15355  sinmpi  15362  cosmpi  15363  sinppi  15364  cosppi  15365  efimpi  15366  sinhalfpip  15367  sinhalfpim  15368  coshalfpip  15369  coshalfpim  15370  ptolemy  15371  tangtx  15385  logdivlti  15428  rpcxpadd  15452  rpmulcxp  15456  rplogbchbase  15497  rprelogbmul  15502  binom4  15526  wilthlem1  15527  1sgmprm  15541  1sgm2ppw  15542  sgmmul  15543  mersenne  15544  perfect1  15545  perfectlem2  15547  perfect  15548  lgsval  15556  lgsfvalg  15557  lgsval2lem  15562  lgsval4a  15574  lgsneg  15576  lgsdilem  15579  lgsdirprm  15586  lgsdir  15587  lgsdilem2  15588  lgsdi  15589  lgsne0  15590  gausslemma2dlem4  15616  gausslemma2dlem6  15619  lgseisenlem2  15623  lgsquadlem1  15629  lgsquadlem2  15630  lgsquadlem3  15631  lgsquad2lem1  15633  lgsquad2lem2  15634  2lgslem3a  15645  2lgslem3b  15646  2lgslem3c  15647  2lgslem3d  15648  2sqlem2  15667  2sqlem3  15669  2sqlem4  15670  2sqlem8  15675  cvgcmp2nlemabs  16112  trilpolemclim  16116  trilpolemcl  16117  trilpolemisumle  16118  trilpolemeq1  16120  trilpolemlt1  16121  trilpo  16123  redcwlpo  16135  nconstwlpolemgt0  16144  nconstwlpo  16146  neapmkv  16148