Theorem oveq12d 5785

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

Syntax hints:   → wi 4   = wceq 1331  (class class class)co 5767

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-v 2683  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-br 3925  df-iota 5083  df-fv 5126  df-ov 5770

This theorem is referenced by:  oveq123d  5788  ovmpodxf  5889  ovmpodf  5895  caovdig  5938  caovdir2d  5940  caovdirg  5941  caovdilemd  5955  caovlem2d  5956  offval  5982  ofvalg  5984  offval2  5990  ofco  5993  caofinvl  5997  offres  6026  nnmsucr  6377  nndir  6379  ecovdi  6533  ecovidi  6534  dfplpq2  7155  dfmpq2  7156  addcmpblnq  7168  mulpipqqs  7174  addassnqg  7183  distrnqg  7188  ltaddnq  7208  halfnqq  7211  enq0tr  7235  addcmpblnq0  7244  addnq0mo  7248  addnnnq0  7250  nqnq0a  7255  distrnq0  7260  addassnq0  7263  distnq0r  7264  nq02m  7266  ltexpri  7414  cauappcvgprlemm  7446  cauappcvgprlemloc  7453  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  cauappcvgprlem1  7460  cauappcvgprlem2  7461  cauappcvgprlemlim  7462  cauappcvgpr  7463  caucvgprlemnkj  7467  caucvgprlemnbj  7468  caucvgprlemm  7469  caucvgprlemloc  7476  caucvgprlemcl  7477  caucvgprlemladdfu  7478  caucvgprlemladdrl  7479  caucvgprlem2  7481  caucvgpr  7483  caucvgprprlemelu  7487  caucvgprprlemcbv  7488  caucvgprprlemval  7489  caucvgprprlemmu  7496  caucvgprprlemopu  7500  caucvgprprlemloc  7504  caucvgprprlemclphr  7506  caucvgprprlemexbt  7507  caucvgprprlem2  7511  mulcmpblnrlemg  7541  mulsrmo  7545  mulsrpr  7547  mulcomsrg  7558  distrsrg  7560  recexgt0sr  7574  mulgt0sr  7579  mulextsr1lem  7581  caucvgsrlemgt1  7596  caucvgsr  7603  addcnsr  7635  mulcnsr  7636  recidpirqlemcalc  7658  axaddcl  7665  axmulcl  7667  axmulcom  7672  axmulass  7674  axdistr  7675  axcaucvglemcau  7699  axcaucvglemres  7700  adddir  7750  muladd11  7888  1p1times  7889  muladd11r  7911  pnpcan2  7995  muladd  8139  subdir  8141  mulsub  8156  mulreim  8359  apadd1  8363  mulext1  8367  recextlem1  8405  muleqadd  8422  divdirap  8450  divadddivap  8480  conjmulap  8482  divcanap5rd  8571  subrecap  8591  xp1d2m1eqxm1d2  8965  div4p1lem1div2  8966  cnref1o  9433  xnegid  9635  xposdif  9658  xleaddadd  9663  icoshftf1o  9767  lincmb01cmp  9779  iccf1o  9780  fz01en  9826  fzrev3  9860  fzrevral2  9879  fzrevral3  9880  fzshftral  9881  fzoaddel2  9963  fzosubel  9964  fzosubel2  9965  fzocatel  9969  modqsubdir  10159  addmodlteq  10164  frecuzrdgsuc  10180  frecfzen2  10193  iseqovex  10222  seqvalcd  10225  seq3caopr3  10247  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  seq3f1olemqsum  10266  seq3id3  10273  seqfeq3  10278  seq3distr  10279  ser3le  10284  mulexp  10325  mulexpzap  10326  expaddzap  10330  expubnd  10343  subsq  10392  binom2  10396  binom21  10397  binom2sub  10398  binom2sub1  10399  binom3  10402  sqoddm1div8  10437  nn0opthlem1d  10459  nn0opthd  10461  facp1  10469  facubnd  10484  bcval  10488  bcn1  10497  bcm1k  10499  bcp1n  10500  bcp1nk  10501  bcval5  10502  bcn2  10503  bcpasc  10505  hashun  10544  hashfz  10560  crre  10622  replim  10624  remullem  10636  remul2  10638  immul2  10645  cjcj  10648  cjadd  10649  ipcnval  10651  cjmulval  10653  cjneg  10655  imval2  10659  cjreim  10668  cvg1nlemcau  10749  cvg1nlemres  10750  resqrexlemp1rp  10771  resqrexlemfp1  10774  resqrexlemcalc1  10779  resqrexlemcalc2  10780  resqrex  10791  sqabsadd  10820  sqabssub  10821  absreimsq  10832  recan  10874  amgm2  10883  maxabslemab  10971  maxabslemval  10973  max0addsup  10984  minabs  11000  bdtrilem  11003  bdtri  11004  xrmaxadd  11023  xrminadd  11037  xrbdtri  11038  subcn2  11073  reccn2ap  11075  climle  11096  climcvg1nlem  11111  serf0  11114  fsumadd  11168  fsumsplit  11169  sumpr  11175  sumtp  11176  isumadd  11193  sumsplitdc  11194  fsum2dlemstep  11196  fsumshftm  11207  fisumrev2  11208  fsumconst  11216  modfsummodlemstep  11219  telfsumo  11228  fsumparts  11232  binomlem  11245  binom  11246  binom1dif  11249  bcxmaslem1  11250  isumsplit  11253  isumnn0nn  11255  arisum  11260  arisum2  11261  trireciplem  11262  trirecip  11263  geosergap  11268  geo2sum  11276  geo2sum2  11277  cvgratnnlemsumlt  11290  mertenslemi1  11297  mertensabs  11299  eftabs  11351  eftvalcn  11352  efcllemp  11353  ege2le3  11366  efcj  11368  efaddlem  11369  efsep  11386  ef4p  11389  efgt1p2  11390  efgt1p  11391  sinval  11398  cosval  11399  tanvalap  11404  tanval2ap  11409  tanval3ap  11410  efi4p  11413  sinneg  11422  cosneg  11423  tannegap  11424  efival  11428  efmival  11429  sinadd  11432  cosadd  11433  tanaddaplem  11434  tanaddap  11435  sinsub  11436  cossub  11437  addsin  11438  subsin  11439  sinmul  11440  cosmul  11441  addcos  11442  subcos  11443  sincossq  11444  cos2t  11446  sin01bnd  11453  cos01bnd  11454  efieq1re  11467  demoivreALT  11469  dvds2ln  11515  odd2np1lem  11558  gcdaddm  11661  bezoutlemnewy  11673  dfgcd3  11687  dvdsgcd  11689  mulgcd  11693  mulgcdr  11695  gcddiv  11696  sqgcd  11706  lcmgcdlem  11747  lcmgcd  11748  qredeu  11767  divgcdcoprm0  11771  cncongr1  11773  oddpwdclemdc  11840  sqrt2irraplemnn  11846  qnumdenbi  11859  zgcdsq  11868  hashdvds  11886  phiprmpw  11887  phimullem  11890  ennnfonelemp1  11908  ressid2  12007  ressval2  12008  topnvalg  12121  topnpropgd  12123  cnfval  12352  cnpfval  12353  ispsmet  12481  psmet0  12485  psmettri2  12486  psmetres2  12491  ismet  12502  isxmet  12503  xmettri2  12519  xmetres2  12537  xblss2  12563  xmstri2  12628  mstri2  12629  xmstri  12630  mstri  12631  xmstri3  12632  mstri3  12633  msrtri  12634  comet  12657  bdxmet  12659  txmetcnp  12676  metcnpd  12678  cnmet  12688  ioo2bl  12701  fsumcncntop  12714  elcncf  12718  mulc1cncf  12734  cncfco  12736  cncfcncntop  12738  cncfmptc  12740  cncfmptid  12741  addccncf  12744  cdivcncfap  12745  negcncf  12746  mulcncflem  12748  limccnp2cntop  12804  reldvg  12806  dvfvalap  12808  eldvap  12809  dvconst  12819  dvaddxxbr  12823  dvmulxxbr  12824  dvcoapbr  12829  dvcjbr  12830  dvexp  12833  dvrecap  12835  dveflem  12844  dvef  12845  sinperlem  12878  sinmpi  12885  cosmpi  12886  sinppi  12887  cosppi  12888  efimpi  12889  sinhalfpip  12890  sinhalfpim  12891  coshalfpip  12892  coshalfpim  12893  ptolemy  12894  tangtx  12908  cvgcmp2nlemabs  13216  trilpolemclim  13218  trilpolemcl  13219  trilpolemisumle  13220  trilpolemeq1  13222  trilpolemlt1  13223  trilpo  13225