Theorem oveq1d 5514

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

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveq1d	⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Proof of Theorem oveq1d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq1 5506	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1243  (class class class)co 5499

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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2309  df-v 2556  df-un 2919  df-sn 3378  df-pr 3379  df-op 3381  df-uni 3578  df-br 3762  df-iota 4854  df-fv 4897  df-ov 5502

This theorem is referenced by:  csbov2g  5533  caovassg  5646  caovdig  5662  caovdirg  5665  caov12d  5669  caov31d  5670  caov411d  5673  grprinvlem  5682  grprinvd  5683  grpridd  5684  caofinvl  5720  omsuc  6038  nnmsucr  6054  nnm1  6084  nnm2  6085  ecovass  6202  ecoviass  6203  ecovdi  6204  ecovidi  6205  addasspig  6409  mulasspig  6411  mulpipq2  6450  distrnqg  6466  ltsonq  6477  ltanqg  6479  ltmnqg  6480  ltexnqq  6487  archnqq  6496  prarloclemarch2  6498  enq0sym  6511  addnq0mo  6526  mulnq0mo  6527  addnnnq0  6528  nqpnq0nq  6532  nq0m0r  6535  nq0a0  6536  nnanq0  6537  distrnq0  6538  addassnq0  6541  addpinq1  6543  prarloclemlo  6573  prarloclem3  6576  prarloclem5  6579  prarloclemcalc  6581  addnqprllem  6606  addnqprulem  6607  appdivnq  6642  recexprlem1ssl  6712  recexprlem1ssu  6713  ltmprr  6721  cauappcvgprlemladdru  6735  cauappcvgprlem1  6738  caucvgprlemnkj  6745  caucvgprlemnbj  6746  caucvgprlemcl  6755  caucvgprlemladdfu  6756  caucvgprlemladdrl  6757  caucvgprlem1  6758  caucvgprprlemcbv  6766  caucvgprprlemval  6767  caucvgprprlemexb  6786  caucvgprprlem1  6788  addcmpblnr  6805  mulcmpblnrlemg  6806  addsrmo  6809  mulsrmo  6810  addsrpr  6811  mulsrpr  6812  ltsrprg  6813  1idsr  6834  pn0sr  6837  recexgt0sr  6839  mulgt0sr  6843  srpospr  6848  prsradd  6851  caucvgsrlemfv  6856  caucvgsrlemcau  6858  caucvgsrlemgt1  6860  caucvgsrlemoffval  6861  caucvgsrlemoffcau  6863  caucvgsrlemoffres  6865  caucvgsrlembnd  6866  caucvgsr  6867  pitonnlem1p1  6903  pitonnlem2  6904  pitonn  6905  recidpirqlemcalc  6914  ax1rid  6932  axrnegex  6934  axcnre  6936  recriota  6945  nntopi  6949  axcaucvglemval  6952  axcaucvglemcau  6953  axcaucvglemres  6954  mul12  7122  mul4  7125  muladd11  7126  readdcan  7133  add12  7149  cnegex  7169  addcan  7171  negeu  7182  pncan2  7198  addsubass  7201  addsub  7202  2addsub  7205  addsubeq4  7206  subid  7209  subid1  7210  npncan  7211  nppcan  7212  nnpcan  7213  nnncan1  7226  npncan3  7228  pnpcan  7229  pnncan  7231  ppncan  7232  addsub4  7233  negsub  7238  subneg  7239  ine0  7370  mulneg1  7371  ltadd2  7395  apreap  7554  cru  7569  recexap  7610  mulcanapd  7618  div23ap  7646  div13ap  7648  divcanap4  7652  divsubdirap  7660  divmuldivap  7664  divdivdivap  7665  divcanap5  7666  divmul13ap  7667  divmuleqap  7669  divdiv32ap  7672  divcanap7  7673  dmdcanap  7674  divdivap1  7675  divdivap2  7676  divadddivap  7679  divsubdivap  7680  conjmulap  7681  divneg2ap  7688  mvllmulapd  7785  lt2mul2div  7821  nndivtr  7931  2halves  8127  halfaddsub  8132  avgle1  8138  avgle2  8139  un0addcl  8187  un0mulcl  8188  peano2z  8253  zneo  8311  nneoor  8312  nneo  8313  zeo  8315  zeo2  8316  deceq1  8342  qreccl  8547  lincmb01cmp  8838  iccf1o  8839  fzosubel3  9019  frecuzrdgsuc  9079  frecfzennn  9081  iseqovex  9097  iseq1p  9117  iseqcaopr2  9119  iseqcaopr  9120  iseqid  9125  iseqhomo  9126  expp1  9140  exprecap  9174  expaddzaplem  9176  expmulzap  9179  expdivap  9183  sqval  9190  sqsubswap  9192  subsq  9236  subsq2  9237  binom2  9240  binom2sub  9242  binom3  9244  zesq  9245  bernneq2  9248  reval  9327  crre  9335  remim  9338  remul2  9351  immul2  9358  imval2  9372  cjdivap  9387  caucvgre  9458  cvg1nlemcau  9461  cvg1nlemres  9462  resqrexlemp1rp  9482  resqrexlemfp1  9485  resqrexlemover  9486  resqrexlemcalc1  9490  resqrexlemcalc3  9492  resqrexlemnm  9494  resqrexlemoverl  9497  resqrexlemglsq  9498  resqrexlemga  9499  resqrexlemsqa  9500  resqrexlemex  9501  resqrex  9502  sqrtdiv  9518  absvalsq  9529  absreimsq  9543  absdivap  9546  cau3lem  9588  clim  9679  clim2  9681  climshftlemg  9700  climshft2  9704  climcn1  9706  climcn2  9707  subcn2  9709  climmulc2  9728  climsubc2  9730  clim2iser  9734  climcau  9743  serif0  9748  sqr2irrlem  9754