Theorem oveq12d 5854

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

Syntax hints:   → wi 4   = wceq 1342  (class class class)co 5836

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 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-rex 2448  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-iota 5147  df-fv 5190  df-ov 5839

This theorem is referenced by:  oveq123d  5857  ovmpodxf  5958  ovmpodf  5964  caovdig  6007  caovdir2d  6009  caovdirg  6010  caovdilemd  6024  caovlem2d  6025  offval  6051  ofvalg  6053  offval2  6059  ofco  6062  caofinvl  6066  offres  6095  nnmsucr  6447  nndir  6449  ecovdi  6603  ecovidi  6604  dfplpq2  7286  dfmpq2  7287  addcmpblnq  7299  mulpipqqs  7305  addassnqg  7314  distrnqg  7319  ltaddnq  7339  halfnqq  7342  enq0tr  7366  addcmpblnq0  7375  addnq0mo  7379  addnnnq0  7381  nqnq0a  7386  distrnq0  7391  addassnq0  7394  distnq0r  7395  nq02m  7397  ltexpri  7545  cauappcvgprlemm  7577  cauappcvgprlemloc  7584  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  cauappcvgprlem1  7591  cauappcvgprlem2  7592  cauappcvgprlemlim  7593  cauappcvgpr  7594  caucvgprlemnkj  7598  caucvgprlemnbj  7599  caucvgprlemm  7600  caucvgprlemloc  7607  caucvgprlemcl  7608  caucvgprlemladdfu  7609  caucvgprlemladdrl  7610  caucvgprlem2  7612  caucvgpr  7614  caucvgprprlemelu  7618  caucvgprprlemcbv  7619  caucvgprprlemval  7620  caucvgprprlemmu  7627  caucvgprprlemopu  7631  caucvgprprlemloc  7635  caucvgprprlemclphr  7637  caucvgprprlemexbt  7638  caucvgprprlem2  7642  mulcmpblnrlemg  7672  mulsrmo  7676  mulsrpr  7678  mulcomsrg  7689  distrsrg  7691  recexgt0sr  7705  mulgt0sr  7710  mulextsr1lem  7712  caucvgsrlemgt1  7727  caucvgsr  7734  addcnsr  7766  mulcnsr  7767  recidpirqlemcalc  7789  axaddcl  7796  axmulcl  7798  axmulcom  7803  axmulass  7805  axdistr  7806  axcaucvglemcau  7830  axcaucvglemres  7831  adddir  7881  muladd11  8022  1p1times  8023  muladd11r  8045  pnpcan2  8129  muladd  8273  subdir  8275  mulsub  8290  mulreim  8493  apadd1  8497  mulext1  8501  recextlem1  8539  muleqadd  8556  divdirap  8584  divadddivap  8614  conjmulap  8616  divcanap5rd  8705  subrecap  8726  xp1d2m1eqxm1d2  9100  div4p1lem1div2  9101  cnref1o  9579  xnegid  9786  xposdif  9809  xleaddadd  9814  icoshftf1o  9918  lincmb01cmp  9930  iccf1o  9931  fz01en  9978  fzrev3  10012  fzrevral2  10031  fzrevral3  10032  fzshftral  10033  fzoaddel2  10118  fzosubel  10119  fzosubel2  10120  fzocatel  10124  modqsubdir  10318  addmodlteq  10323  frecuzrdgsuc  10339  frecfzen2  10352  iseqovex  10381  seqvalcd  10384  seq3caopr3  10406  seq3f1olemqsumkj  10423  seq3f1olemqsumk  10424  seq3f1olemqsum  10425  seq3id3  10432  seqfeq3  10437  seq3distr  10438  ser3le  10443  mulexp  10484  mulexpzap  10485  expaddzap  10489  expubnd  10502  subsq  10551  binom2  10555  binom21  10556  binom2sub  10557  binom2sub1  10558  binom3  10561  sqoddm1div8  10597  nn0opthlem1d  10622  nn0opthd  10624  facp1  10632  facubnd  10647  bcval  10651  bcn1  10660  bcm1k  10662  bcp1n  10663  bcp1nk  10664  bcval5  10665  bcn2  10666  bcpasc  10668  hashun  10707  hashfz  10723  crre  10785  replim  10787  remullem  10799  remul2  10801  immul2  10808  cjcj  10811  cjadd  10812  ipcnval  10814  cjmulval  10816  cjneg  10818  imval2  10822  cjreim  10831  cvg1nlemcau  10912  cvg1nlemres  10913  resqrexlemp1rp  10934  resqrexlemfp1  10937  resqrexlemcalc1  10942  resqrexlemcalc2  10943  resqrex  10954  sqabsadd  10983  sqabssub  10984  absreimsq  10995  recan  11037  amgm2  11046  maxabslemab  11134  maxabslemval  11136  max0addsup  11147  minabs  11163  bdtrilem  11166  bdtri  11167  xrmaxadd  11188  xrminadd  11202  xrbdtri  11203  subcn2  11238  reccn2ap  11240  climle  11261  climcvg1nlem  11276  serf0  11279  fsumadd  11333  fsumsplit  11334  sumpr  11340  sumtp  11341  isumadd  11358  sumsplitdc  11359  fsum2dlemstep  11361  fsumshftm  11372  fisumrev2  11373  fsumconst  11381  modfsummodlemstep  11384  telfsumo  11393  fsumparts  11397  binomlem  11410  binom  11411  binom1dif  11414  bcxmaslem1  11415  isumsplit  11418  isumnn0nn  11420  arisum  11425  arisum2  11426  trireciplem  11427  trirecip  11428  geosergap  11433  geo2sum  11441  geo2sum2  11442  cvgratnnlemsumlt  11455  mertenslemi1  11462  mertensabs  11464  fprodmul  11518  fprodsplitdc  11523  fprodabs  11543  fprod2dlemstep  11549  fproddivapf  11558  eftabs  11583  eftvalcn  11584  efcllemp  11585  ege2le3  11598  efcj  11600  efaddlem  11601  efsep  11618  ef4p  11621  efgt1p2  11622  efgt1p  11623  sinval  11629  cosval  11630  tanvalap  11635  tanval2ap  11640  tanval3ap  11641  efi4p  11644  sinneg  11653  cosneg  11654  tannegap  11655  efival  11659  efmival  11660  sinadd  11663  cosadd  11664  tanaddaplem  11665  tanaddap  11666  sinsub  11667  cossub  11668  addsin  11669  subsin  11670  sinmul  11671  cosmul  11672  addcos  11673  subcos  11674  sincossq  11675  cos2t  11677  sin01bnd  11684  cos01bnd  11685  efieq1re  11698  demoivreALT  11700  dvds2ln  11750  odd2np1lem  11794  gcdaddm  11902  bezoutlemnewy  11914  dfgcd3  11928  dvdsgcd  11930  mulgcd  11934  mulgcdr  11936  gcddiv  11937  sqgcd  11947  lcmgcdlem  11988  lcmgcd  11989  qredeu  12008  divgcdcoprm0  12012  cncongr1  12014  oddpwdclemdc  12082  sqrt2irraplemnn  12088  qnumdenbi  12101  zgcdsq  12110  hashdvds  12130  phiprmpw  12131  phimullem  12134  eulerthlema  12139  prmdiv  12144  modprm0  12163  coprimeprodsq  12166  pythagtriplem1  12174  pythagtriplem12  12184  pythagtriplem14  12186  pythagtriplem15  12187  pythagtriplem16  12188  pythagtriplem17  12189  pythagtriplem19  12191  pcval  12205  pcmul  12210  pcdiv  12211  pcqmul  12212  pcid  12232  pcaddlem  12247  pcmpt  12250  pcmpt2  12251  pcmptdvds  12252  pcbc  12258  ennnfonelemp1  12276  nninfdclemp1  12322  ressid2  12390  ressval2  12391  topnvalg  12504  topnpropgd  12506  cnfval  12735  cnpfval  12736  ispsmet  12864  psmet0  12868  psmettri2  12869  psmetres2  12874  ismet  12885  isxmet  12886  xmettri2  12902  xmetres2  12920  xblss2  12946  xmstri2  13011  mstri2  13012  xmstri  13013  mstri  13014  xmstri3  13015  mstri3  13016  msrtri  13017  comet  13040  bdxmet  13042  txmetcnp  13059  metcnpd  13061  cnmet  13071  ioo2bl  13084  fsumcncntop  13097  elcncf  13101  mulc1cncf  13117  cncfco  13119  cncfcncntop  13121  cncfmptc  13123  cncfmptid  13124  addccncf  13127  cdivcncfap  13128  negcncf  13129  mulcncflem  13131  limccnp2cntop  13187  reldvg  13189  dvfvalap  13191  eldvap  13192  dvconst  13202  dvaddxxbr  13206  dvmulxxbr  13207  dvcoapbr  13212  dvcjbr  13213  dvexp  13216  dvrecap  13218  dveflem  13228  dvef  13229  sinperlem  13270  sinmpi  13277  cosmpi  13278  sinppi  13279  cosppi  13280  efimpi  13281  sinhalfpip  13282  sinhalfpim  13283  coshalfpip  13284  coshalfpim  13285  ptolemy  13286  tangtx  13300  logdivlti  13343  rpcxpadd  13367  rpmulcxp  13371  rplogbchbase  13409  rprelogbmul  13414  binom4  13438  cvgcmp2nlemabs  13745  trilpolemclim  13749  trilpolemcl  13750  trilpolemisumle  13751  trilpolemeq1  13753  trilpolemlt1  13754  trilpo  13756  redcwlpo  13768  nconstwlpolemgt0  13776  nconstwlpo  13778  neapmkv  13780