Theorem oveq12d 5887

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

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

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 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-iota 5174  df-fv 5220  df-ov 5872

This theorem is referenced by:  oveq123d  5890  ovmpodxf  5994  ovmpodf  6000  caovdig  6043  caovdir2d  6045  caovdirg  6046  caovdilemd  6060  caovlem2d  6061  offval  6084  ofvalg  6086  offval2  6092  ofco  6095  caofinvl  6099  offres  6130  nnmsucr  6483  nndir  6485  ecovdi  6640  ecovidi  6641  dfplpq2  7344  dfmpq2  7345  addcmpblnq  7357  mulpipqqs  7363  addassnqg  7372  distrnqg  7377  ltaddnq  7397  halfnqq  7400  enq0tr  7424  addcmpblnq0  7433  addnq0mo  7437  addnnnq0  7439  nqnq0a  7444  distrnq0  7449  addassnq0  7452  distnq0r  7453  nq02m  7455  ltexpri  7603  cauappcvgprlemm  7635  cauappcvgprlemloc  7642  cauappcvgprlemladdru  7646  cauappcvgprlemladdrl  7647  cauappcvgprlem1  7649  cauappcvgprlem2  7650  cauappcvgprlemlim  7651  cauappcvgpr  7652  caucvgprlemnkj  7656  caucvgprlemnbj  7657  caucvgprlemm  7658  caucvgprlemloc  7665  caucvgprlemcl  7666  caucvgprlemladdfu  7667  caucvgprlemladdrl  7668  caucvgprlem2  7670  caucvgpr  7672  caucvgprprlemelu  7676  caucvgprprlemcbv  7677  caucvgprprlemval  7678  caucvgprprlemmu  7685  caucvgprprlemopu  7689  caucvgprprlemloc  7693  caucvgprprlemclphr  7695  caucvgprprlemexbt  7696  caucvgprprlem2  7700  mulcmpblnrlemg  7730  mulsrmo  7734  mulsrpr  7736  mulcomsrg  7747  distrsrg  7749  recexgt0sr  7763  mulgt0sr  7768  mulextsr1lem  7770  caucvgsrlemgt1  7785  caucvgsr  7792  addcnsr  7824  mulcnsr  7825  recidpirqlemcalc  7847  axaddcl  7854  axmulcl  7856  axmulcom  7861  axmulass  7863  axdistr  7864  axcaucvglemcau  7888  axcaucvglemres  7889  adddir  7939  muladd11  8080  1p1times  8081  muladd11r  8103  pnpcan2  8187  muladd  8331  subdir  8333  mulsub  8348  mulreim  8551  apadd1  8555  mulext1  8559  recextlem1  8597  muleqadd  8614  divdirap  8643  divadddivap  8673  conjmulap  8675  divcanap5rd  8764  subrecap  8785  xp1d2m1eqxm1d2  9160  div4p1lem1div2  9161  cnref1o  9639  xnegid  9846  xposdif  9869  xleaddadd  9874  icoshftf1o  9978  lincmb01cmp  9990  iccf1o  9991  fz01en  10039  fzrev3  10073  fzrevral2  10092  fzrevral3  10093  fzshftral  10094  fzoaddel2  10179  fzosubel  10180  fzosubel2  10181  fzocatel  10185  modqsubdir  10379  addmodlteq  10384  frecuzrdgsuc  10400  frecfzen2  10413  iseqovex  10442  seqvalcd  10445  seq3caopr3  10467  seq3f1olemqsumkj  10484  seq3f1olemqsumk  10485  seq3f1olemqsum  10486  seq3id3  10493  seqfeq3  10498  seq3distr  10499  ser3le  10504  mulexp  10545  mulexpzap  10546  expaddzap  10550  expubnd  10563  subsq  10612  binom2  10617  binom21  10618  binom2sub  10619  binom2sub1  10620  binom3  10623  sqoddm1div8  10659  nn0opthlem1d  10684  nn0opthd  10686  facp1  10694  facubnd  10709  bcval  10713  bcn1  10722  bcm1k  10724  bcp1n  10725  bcp1nk  10726  bcval5  10727  bcn2  10728  bcpasc  10730  hashun  10769  hashfz  10785  crre  10850  replim  10852  remullem  10864  remul2  10866  immul2  10873  cjcj  10876  cjadd  10877  ipcnval  10879  cjmulval  10881  cjneg  10883  imval2  10887  cjreim  10896  cvg1nlemcau  10977  cvg1nlemres  10978  resqrexlemp1rp  10999  resqrexlemfp1  11002  resqrexlemcalc1  11007  resqrexlemcalc2  11008  resqrex  11019  sqabsadd  11048  sqabssub  11049  absreimsq  11060  recan  11102  amgm2  11111  maxabslemab  11199  maxabslemval  11201  max0addsup  11212  minabs  11228  bdtrilem  11231  bdtri  11232  xrmaxadd  11253  xrminadd  11267  xrbdtri  11268  subcn2  11303  reccn2ap  11305  climle  11326  climcvg1nlem  11341  serf0  11344  fsumadd  11398  fsumsplit  11399  sumpr  11405  sumtp  11406  isumadd  11423  sumsplitdc  11424  fsum2dlemstep  11426  fsumshftm  11437  fisumrev2  11438  fsumconst  11446  modfsummodlemstep  11449  telfsumo  11458  fsumparts  11462  binomlem  11475  binom  11476  binom1dif  11479  bcxmaslem1  11480  isumsplit  11483  isumnn0nn  11485  arisum  11490  arisum2  11491  trireciplem  11492  trirecip  11493  geosergap  11498  geo2sum  11506  geo2sum2  11507  cvgratnnlemsumlt  11520  mertenslemi1  11527  mertensabs  11529  fprodmul  11583  fprodsplitdc  11588  fprodabs  11608  fprod2dlemstep  11614  fproddivapf  11623  eftabs  11648  eftvalcn  11649  efcllemp  11650  ege2le3  11663  efcj  11665  efaddlem  11666  efsep  11683  ef4p  11686  efgt1p2  11687  efgt1p  11688  sinval  11694  cosval  11695  tanvalap  11700  tanval2ap  11705  tanval3ap  11706  efi4p  11709  sinneg  11718  cosneg  11719  tannegap  11720  efival  11724  efmival  11725  sinadd  11728  cosadd  11729  tanaddaplem  11730  tanaddap  11731  sinsub  11732  cossub  11733  addsin  11734  subsin  11735  sinmul  11736  cosmul  11737  addcos  11738  subcos  11739  sincossq  11740  cos2t  11742  sin01bnd  11749  cos01bnd  11750  efieq1re  11763  demoivreALT  11765  dvds2ln  11815  odd2np1lem  11860  gcdaddm  11968  bezoutlemnewy  11980  dfgcd3  11994  dvdsgcd  11996  mulgcd  12000  mulgcdr  12002  gcddiv  12003  sqgcd  12013  lcmgcdlem  12060  lcmgcd  12061  qredeu  12080  divgcdcoprm0  12084  cncongr1  12086  oddpwdclemdc  12156  sqrt2irraplemnn  12162  qnumdenbi  12175  zgcdsq  12184  hashdvds  12204  phiprmpw  12205  phimullem  12208  eulerthlema  12213  prmdiv  12218  modprm0  12237  coprimeprodsq  12240  pythagtriplem1  12248  pythagtriplem12  12258  pythagtriplem14  12260  pythagtriplem15  12261  pythagtriplem16  12262  pythagtriplem17  12263  pythagtriplem19  12265  pcval  12279  pcmul  12284  pcdiv  12285  pcqmul  12286  pcid  12306  pcaddlem  12321  pcmpt  12324  pcmpt2  12325  pcmptdvds  12326  pcbc  12332  4sqlem4  12373  mul4sqlem  12374  mul4sq  12375  ennnfonelemp1  12390  nninfdclemp1  12434  ressvalsets  12506  topnvalg  12648  topnpropgd  12650  ismhm  12743  mhmf1o  12751  0mhm  12763  mhmco  12764  mhmeql  12766  isgrpid2  12803  grpnpcan  12851  mhmmnd  12869  mulgnndir  12900  mulgdir  12903  ablsub4  12943  mgpvalg  12960  mgptopng  12966  srglmhm  13002  srgrmhm  13003  rngo2times  13037  ringcom  13040  ringpropd  13043  ring1  13062  opprvalg  13066  opprring  13074  invrfvald  13116  dvrvald  13128  cnfval  13361  cnpfval  13362  ispsmet  13490  psmet0  13494  psmettri2  13495  psmetres2  13500  ismet  13511  isxmet  13512  xmettri2  13528  xmetres2  13546  xblss2  13572  xmstri2  13637  mstri2  13638  xmstri  13639  mstri  13640  xmstri3  13641  mstri3  13642  msrtri  13643  comet  13666  bdxmet  13668  txmetcnp  13685  metcnpd  13687  cnmet  13697  ioo2bl  13710  fsumcncntop  13723  elcncf  13727  mulc1cncf  13743  cncfco  13745  cncfcncntop  13747  cncfmptc  13749  cncfmptid  13750  addccncf  13753  cdivcncfap  13754  negcncf  13755  mulcncflem  13757  limccnp2cntop  13813  reldvg  13815  dvfvalap  13817  eldvap  13818  dvconst  13828  dvaddxxbr  13832  dvmulxxbr  13833  dvcoapbr  13838  dvcjbr  13839  dvexp  13842  dvrecap  13844  dveflem  13854  dvef  13855  sinperlem  13896  sinmpi  13903  cosmpi  13904  sinppi  13905  cosppi  13906  efimpi  13907  sinhalfpip  13908  sinhalfpim  13909  coshalfpip  13910  coshalfpim  13911  ptolemy  13912  tangtx  13926  logdivlti  13969  rpcxpadd  13993  rpmulcxp  13997  rplogbchbase  14035  rprelogbmul  14040  binom4  14064  lgsval  14072  lgsfvalg  14073  lgsval2lem  14078  lgsval4a  14090  lgsneg  14092  lgsdilem  14095  lgsdirprm  14102  lgsdir  14103  lgsdilem2  14104  lgsdi  14105  lgsne0  14106  2sqlem2  14118  2sqlem3  14120  2sqlem4  14121  2sqlem8  14126  cvgcmp2nlemabs  14436  trilpolemclim  14440  trilpolemcl  14441  trilpolemisumle  14442  trilpolemeq1  14444  trilpolemlt1  14445  trilpo  14447  redcwlpo  14459  nconstwlpolemgt0  14467  nconstwlpo  14469  neapmkv  14471