Theorem opreq2d 3013

Description: Equality deduction for operations.

Hypothesis

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

Assertion

Ref	Expression
opreq2d	⊢ (φ → (CFA) = (CFB))

Proof of Theorem opreq2d

Step	Hyp	Ref	Expression
1		opreq1d.1	. 2 ⊢ (φ → A = B)
2		opreq2 3007	. 2 ⊢ (A = B → (CFA) = (CFB))
3	1, 2	syl 12	1 ⊢ (φ → (CFA) = (CFB))

Syntax hints:   → wi 2   = wceq 1091  (class class class)co 3001

This theorem is referenced by:  opreq12d 3014  caoprass 3068  caoprdistr 3073  oaass 3163  nndi 3180  nnmass 3181  nnmsucr 3182  ecoprass 3256  ecoprdi 3257  addasspi 3817  mulasspi 3819  distrpi 3820  addclprlem2 3913  mulclprlem 3915  distrlem4pr 3924  1idpr 3927  prlem934a 3931  prlem936a 3947  prlem936 3949  mulcmpblnrlem 3976  ssgt0sr 4011  supsrlem4 4022  supsr 4025  mulcnsr 4048  ax1id 4077  axcnre 4087  add23t 4126  subnegt 4149  addsubasst 4150  subneg2t 4158  pncant 4161  mul23t 4176  subdit 4184  mul2negt 4199  negdit 4200  negdi2t 4201  subsubt 4203  divcan2t 4229  divrecz 4237  divrect 4238  divasst 4239  divdistrt 4246  recrect 4260  divadddivt 4264  divdivdivt 4265  nnmulclt 4437  cru 4529  crut 4531  creur 4532  creui 4533  uzind 4603  seqval 4665  seqsuclem 4669  expvalt 4677  expp1t 4678  expaddt 4698  discrlem2 4714  discrlem3 4715  discrlem 4716  nn0opth 4724  sqrmul 4763  sqr2irrlem2 4778  sqr2irrlem3 4779  sqr2irrlem5 4781  replimt 4798  reim0 4809  rere 4810  cjaddt 4831  cjmult 4832  abs00 4839  absmult 4849  abslem2 4867  facp1t 4873  ruclem4 4888  ruclem32 4916  hvsubvalt 4997  hvadd23t 5011  hvsub4t 5014  hvaddsub12t 5015  hvsubcan1t 5016  hvaddsubasst 5018  hvsubsub4t 5032  hvnegdit 5039  his5 5050  his2subt 5052  normlem6 5068  norm-iiit 5088  normpyth 5090  normpytht 5092  norm3adift 5098  bcs 5101  chocuni 5179  occllem2 5181  projlem7 5199  projlem17 5209  projlem20 5212  projlem22 5214  projlem26 5218  pjthlem8 5232  pjthlem9 5233  omlsilem 5249  pjch 5269  chdmm1t 5438  chdmm3t 5440  chdmm4t 5441  chjasst 5446  h1de2b 5459  spanunsn 5482  hosmvalt 5487  hodmvalt 5488  cmcmlem 5500  spansnjt 5540  spansncvt 5543  5oalem1 5544  5oalem2 5545  5oalem3 5546  5oalem5 5548  3oalem2 5553  pjcj 5575  pjadjt 5576  pjaddt 5577  pjsubt 5578  pjmult 5579  pjcjt2 5580  hosass 5607  hoid0 5614  pjadjco 5631  pjss2co 5634  pjclem4 5653  pjadj2co 5656  pj3s 5659  pj3cor1 5661  pjopytht 5662  stjt 5676  st0 5690  stcltrlem1 5709  mdbr 5726  dmdbr 5731  ssmd1 5734  ssmd2 5735  cvexchlem 5759  atcvat3 5774

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-xp 2424  df-cnv 2426  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fv 2438  df-opr 3003

metamath.org