Theorem oveq1d 5470

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
oveq1d	⊢ (φ → (A𝐹𝐶) = (B𝐹𝐶))

Proof of Theorem oveq1d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (φ → A = B)
2		oveq1 5462	. 2 ⊢ (A = B → (A𝐹𝐶) = (B𝐹𝐶))
3	1, 2	syl 14	1 ⊢ (φ → (A𝐹𝐶) = (B𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1242  (class class class)co 5455

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458

This theorem is referenced by:  csbov2g  5488  caovassg  5601  caovdig  5617  caovdirg  5620  caov12d  5624  caov31d  5625  caov411d  5628  grprinvlem  5637  grprinvd  5638  grpridd  5639  caofinvl  5675  omsuc  5990  nnmsucr  6006  nnm1  6033  nnm2  6034  ecovass  6151  ecoviass  6152  ecovdi  6153  ecovidi  6154  addasspig  6314  mulasspig  6316  mulpipq2  6355  distrnqg  6371  ltsonq  6382  ltanqg  6384  ltmnqg  6385  ltexnqq  6391  archnqq  6400  prarloclemarch2  6402  enq0sym  6415  addnq0mo  6430  mulnq0mo  6431  addnnnq0  6432  nqpnq0nq  6436  nq0m0r  6439  nq0a0  6440  nnanq0  6441  distrnq0  6442  addassnq0  6445  addpinq1  6447  prarloclemlo  6477  prarloclem3  6480  prarloclem5  6483  prarloclemcalc  6485  addnqprllem  6510  addnqprulem  6511  appdivnq  6544  recexprlem1ssl  6605  recexprlem1ssu  6606  ltmprr  6614  cauappcvgprlemladdru  6628  cauappcvgprlem1  6631  caucvgprlemnkj  6637  caucvgprlemnbj  6638  caucvgprlemcl  6647  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlem1  6650  addcmpblnr  6667  mulcmpblnrlemg  6668  addsrmo  6671  mulsrmo  6672  addsrpr  6673  mulsrpr  6674  ltsrprg  6675  1idsr  6696  pn0sr  6699  recexgt0sr  6701  mulgt0sr  6704  pitonnlem1p1  6742  pitonnlem2  6743  pitonn  6744  ax1rid  6761  axrnegex  6763  axcnre  6765  mul12  6939  mul4  6942  muladd11  6943  readdcan  6950  add12  6966  cnegex  6986  addcan  6988  negeu  6999  pncan2  7015  addsubass  7018  addsub  7019  2addsub  7022  addsubeq4  7023  subid  7026  subid1  7027  npncan  7028  nppcan  7029  nnpcan  7030  nnncan1  7043  npncan3  7045  pnpcan  7046  pnncan  7048  ppncan  7049  addsub4  7050  negsub  7055  subneg  7056  ine0  7187  mulneg1  7188  ltadd2  7212  apreap  7371  cru  7386  recexap  7416  mulcanapd  7424  div23ap  7452  div13ap  7454  divcanap4  7458  divsubdirap  7466  divmuldivap  7470  divdivdivap  7471  divcanap5  7472  divmul13ap  7473  divmuleqap  7475  divdiv32ap  7478  divcanap7  7479  dmdcanap  7480  divdivap1  7481  divdivap2  7482  divadddivap  7485  divsubdivap  7486  conjmulap  7487  divneg2ap  7494  mvllmulapd  7590  lt2mul2div  7626  nndivtr  7736  2halves  7931  halfaddsub  7936  avgle1  7942  avgle2  7943  un0addcl  7991  un0mulcl  7992  peano2z  8057  zneo  8115  nneoor  8116  nneo  8117  zeo  8119  zeo2  8120  deceq1  8146  qreccl  8351  lincmb01cmp  8641  iccf1o  8642  fzosubel3  8822  frecuzrdgsuc  8882  frecfzennn  8884  iseqovex  8899  expp1  8916  exprecap  8950  expaddzaplem  8952  expmulzap  8955  expdivap  8959  sqval  8966  sqsubswap  8968  subsq  9011  subsq2  9012  binom2  9015  binom2sub  9017  binom3  9019  zesq  9020  bernneq2  9023  reval  9077  crre  9085  remim  9088  remul2  9101  immul2  9108  imval2  9122  cjdivap  9137