Theorem oveq12d 5893

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

Syntax hints:   → wi 4   = wceq 1353  (class class class)co 5875

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878

This theorem is referenced by:  oveq123d  5896  ovmpodxf  6000  ovmpodf  6006  caovdig  6049  caovdir2d  6051  caovdirg  6052  caovdilemd  6066  caovlem2d  6067  offval  6090  ofvalg  6092  offval2  6098  ofco  6101  caofinvl  6105  offres  6136  nnmsucr  6489  nndir  6491  ecovdi  6646  ecovidi  6647  dfplpq2  7353  dfmpq2  7354  addcmpblnq  7366  mulpipqqs  7372  addassnqg  7381  distrnqg  7386  ltaddnq  7406  halfnqq  7409  enq0tr  7433  addcmpblnq0  7442  addnq0mo  7446  addnnnq0  7448  nqnq0a  7453  distrnq0  7458  addassnq0  7461  distnq0r  7462  nq02m  7464  ltexpri  7612  cauappcvgprlemm  7644  cauappcvgprlemloc  7651  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  cauappcvgprlem2  7659  cauappcvgprlemlim  7660  cauappcvgpr  7661  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemloc  7674  caucvgprlemcl  7675  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgprlem2  7679  caucvgpr  7681  caucvgprprlemelu  7685  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemmu  7694  caucvgprprlemopu  7698  caucvgprprlemloc  7702  caucvgprprlemclphr  7704  caucvgprprlemexbt  7705  caucvgprprlem2  7709  mulcmpblnrlemg  7739  mulsrmo  7743  mulsrpr  7745  mulcomsrg  7756  distrsrg  7758  recexgt0sr  7772  mulgt0sr  7777  mulextsr1lem  7779  caucvgsrlemgt1  7794  caucvgsr  7801  addcnsr  7833  mulcnsr  7834  recidpirqlemcalc  7856  axaddcl  7863  axmulcl  7865  axmulcom  7870  axmulass  7872  axdistr  7873  axcaucvglemcau  7897  axcaucvglemres  7898  adddir  7948  muladd11  8090  1p1times  8091  muladd11r  8113  pnpcan2  8197  muladd  8341  subdir  8343  mulsub  8358  mulreim  8561  apadd1  8565  mulext1  8569  recextlem1  8608  muleqadd  8625  divdirap  8654  divadddivap  8684  conjmulap  8686  divcanap5rd  8775  subrecap  8796  xp1d2m1eqxm1d2  9171  div4p1lem1div2  9172  cnref1o  9650  xnegid  9859  xposdif  9882  xleaddadd  9887  icoshftf1o  9991  lincmb01cmp  10003  iccf1o  10004  fz01en  10053  fzrev3  10087  fzrevral2  10106  fzrevral3  10107  fzshftral  10108  fzoaddel2  10193  fzosubel  10194  fzosubel2  10195  fzocatel  10199  modqsubdir  10393  addmodlteq  10398  frecuzrdgsuc  10414  frecfzen2  10427  iseqovex  10456  seqvalcd  10459  seq3caopr3  10481  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3f1olemqsum  10500  seq3id3  10507  seqfeq3  10512  seq3distr  10513  ser3le  10518  mulexp  10559  mulexpzap  10560  expaddzap  10564  expubnd  10577  subsq  10627  binom2  10632  binom21  10633  binom2sub  10634  binom2sub1  10635  binom3  10638  sqoddm1div8  10674  mulsubdivbinom2ap  10691  nn0opthlem1d  10700  nn0opthd  10702  facp1  10710  facubnd  10725  bcval  10729  bcn1  10738  bcm1k  10740  bcp1n  10741  bcp1nk  10742  bcval5  10743  bcn2  10744  bcpasc  10746  hashun  10785  hashfz  10801  crre  10866  replim  10868  remullem  10880  remul2  10882  immul2  10889  cjcj  10892  cjadd  10893  ipcnval  10895  cjmulval  10897  cjneg  10899  imval2  10903  cjreim  10912  cvg1nlemcau  10993  cvg1nlemres  10994  resqrexlemp1rp  11015  resqrexlemfp1  11018  resqrexlemcalc1  11023  resqrexlemcalc2  11024  resqrex  11035  sqabsadd  11064  sqabssub  11065  absreimsq  11076  recan  11118  amgm2  11127  maxabslemab  11215  maxabslemval  11217  max0addsup  11228  minabs  11244  bdtrilem  11247  bdtri  11248  xrmaxadd  11269  xrminadd  11283  xrbdtri  11284  subcn2  11319  reccn2ap  11321  climle  11342  climcvg1nlem  11357  serf0  11360  fsumadd  11414  fsumsplit  11415  sumpr  11421  sumtp  11422  isumadd  11439  sumsplitdc  11440  fsum2dlemstep  11442  fsumshftm  11453  fisumrev2  11454  fsumconst  11462  modfsummodlemstep  11465  telfsumo  11474  fsumparts  11478  binomlem  11491  binom  11492  binom1dif  11495  bcxmaslem1  11496  isumsplit  11499  isumnn0nn  11501  arisum  11506  arisum2  11507  trireciplem  11508  trirecip  11509  geosergap  11514  geo2sum  11522  geo2sum2  11523  cvgratnnlemsumlt  11536  mertenslemi1  11543  mertensabs  11545  fprodmul  11599  fprodsplitdc  11604  fprodabs  11624  fprod2dlemstep  11630  fproddivapf  11639  eftabs  11664  eftvalcn  11665  efcllemp  11666  ege2le3  11679  efcj  11681  efaddlem  11682  efsep  11699  ef4p  11702  efgt1p2  11703  efgt1p  11704  sinval  11710  cosval  11711  tanvalap  11716  tanval2ap  11721  tanval3ap  11722  efi4p  11725  sinneg  11734  cosneg  11735  tannegap  11736  efival  11740  efmival  11741  sinadd  11744  cosadd  11745  tanaddaplem  11746  tanaddap  11747  sinsub  11748  cossub  11749  addsin  11750  subsin  11751  sinmul  11752  cosmul  11753  addcos  11754  subcos  11755  sincossq  11756  cos2t  11758  sin01bnd  11765  cos01bnd  11766  efieq1re  11779  demoivreALT  11781  dvds2ln  11831  odd2np1lem  11877  gcdaddm  11985  bezoutlemnewy  11997  dfgcd3  12011  dvdsgcd  12013  mulgcd  12017  mulgcdr  12019  gcddiv  12020  sqgcd  12030  lcmgcdlem  12077  lcmgcd  12078  qredeu  12097  divgcdcoprm0  12101  cncongr1  12103  oddpwdclemdc  12173  sqrt2irraplemnn  12179  qnumdenbi  12192  zgcdsq  12201  hashdvds  12221  phiprmpw  12222  phimullem  12225  eulerthlema  12230  prmdiv  12235  modprm0  12254  coprimeprodsq  12257  pythagtriplem1  12265  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem15  12278  pythagtriplem16  12279  pythagtriplem17  12280  pythagtriplem19  12282  pcval  12296  pcmul  12301  pcdiv  12302  pcqmul  12303  pcid  12323  pcaddlem  12338  pcmpt  12341  pcmpt2  12342  pcmptdvds  12343  pcbc  12349  4sqlem4  12390  mul4sqlem  12391  mul4sq  12392  ennnfonelemp1  12407  nninfdclemp1  12451  ressvalsets  12524  topnvalg  12700  topnpropgd  12702  prdsex  12718  qusval  12744  qusaddvallemg  12752  xpsval  12771  ismhm  12853  mhmf1o  12861  0mhm  12873  mhmco  12874  mhmeql  12876  isgrpid2  12913  grpnpcan  12962  mhmmnd  12980  mulgnndir  13012  mulgdir  13015  isnsg3  13067  ablsub4  13116  mgpvalg  13133  mgptopng  13139  mgpress  13141  srglmhm  13176  srgrmhm  13177  ringo2times  13211  ringcom  13214  ringpropd  13217  ring1  13236  opprvalg  13241  opprring  13249  invrfvald  13291  dvrvald  13303  dvrdir  13312  rdivmuldivd  13313  islmod  13381  lmodlema  13382  islmodd  13383  lmodcom  13423  lmodnegadd  13426  lmodprop2d  13438  rmodislmod  13441  cnfval  13697  cnpfval  13698  ispsmet  13826  psmet0  13830  psmettri2  13831  psmetres2  13836  ismet  13847  isxmet  13848  xmettri2  13864  xmetres2  13882  xblss2  13908  xmstri2  13973  mstri2  13974  xmstri  13975  mstri  13976  xmstri3  13977  mstri3  13978  msrtri  13979  comet  14002  bdxmet  14004  txmetcnp  14021  metcnpd  14023  cnmet  14033  ioo2bl  14046  fsumcncntop  14059  elcncf  14063  mulc1cncf  14079  cncfco  14081  cncfcncntop  14083  cncfmptc  14085  cncfmptid  14086  addccncf  14089  cdivcncfap  14090  negcncf  14091  mulcncflem  14093  limccnp2cntop  14149  reldvg  14151  dvfvalap  14153  eldvap  14154  dvconst  14164  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  dvcjbr  14175  dvexp  14178  dvrecap  14180  dveflem  14190  dvef  14191  sinperlem  14232  sinmpi  14239  cosmpi  14240  sinppi  14241  cosppi  14242  efimpi  14243  sinhalfpip  14244  sinhalfpim  14245  coshalfpip  14246  coshalfpim  14247  ptolemy  14248  tangtx  14262  logdivlti  14305  rpcxpadd  14329  rpmulcxp  14333  rplogbchbase  14371  rprelogbmul  14376  binom4  14400  lgsval  14408  lgsfvalg  14409  lgsval2lem  14414  lgsval4a  14426  lgsneg  14428  lgsdilem  14431  lgsdirprm  14438  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgseisenlem2  14454  2sqlem2  14465  2sqlem3  14467  2sqlem4  14468  2sqlem8  14473  cvgcmp2nlemabs  14783  trilpolemclim  14787  trilpolemcl  14788  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  trilpo  14794  redcwlpo  14806  nconstwlpolemgt0  14814  nconstwlpo  14816  neapmkv  14818