Theorem opreq1d 3012

Description: Equality deduction for operations.

Hypothesis

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

Assertion

Ref	Expression
opreq1d	⊢ (φ → (AFC) = (BFC))

Proof of Theorem opreq1d

Step	Hyp	Ref	Expression
1		opreq1d.1	. 2 ⊢ (φ → A = B)
2		opreq1 3006	. 2 ⊢ (A = B → (AFC) = (BFC))
3	1, 2	syl 12	1 ⊢ (φ → (AFC) = (BFC))

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

This theorem is referenced by:  opreq12d 3014  caoprass 3068  caoprdistr 3073  om1 3144  oe1 3146  nnmsucr 3182  ecoprass 3256  ecoprdi 3257  addasspi 3817  mulasspi 3819  addclprlem1 3912  prlem934a 3931  reclem3pr 3952  mulcmpblnrlem 3976  1idsr 4001  pn0sr 4004  recexsrlem 4006  mulgt0sr 4008  ssgt0sr 4011  supsrlem2 4020  ax1id 4077  axcnre 4087  add12t 4125  add4t 4127  addsubt 4151  mul4t 4177  subdit 4184  mulneg1t 4196  mul2negt 4199  negdit 4200  divcan1t 4228  div23t 4240  divdistrt 4246  divcan3t 4251  divmuldivt 4263  divadddivt 4264  divdivdivt 4265  divdiv23t 4271  nnsub 4450  ine0 4524  zneo 4601  uzind 4603  flleltt 4625  qrecclt 4646  om2uzsuc 4652  uzrdgsuc 4659  seqlem1 4662  seqrval 4664  seqsuclem 4669  expp1t 4678  exp2t 4683  discrlem2 4714  discrlem3 4715  discrlem 4716  nneo 4719  nn0opth 4724  nn0opth2t 4726  sqrlem21 4751  sqrmul 4763  sqsqrt 4776  sqr2irrlem2 4778  replimt 4798  cjvalt 4799  cjaddt 4831  cjmult 4832  absmult 4849  facp1t 4873  clim 4877  clim2 4881  clim0 4882  ruclem4 4888  ruclem32 4916  xpnnen 4927  znnenlem 4929  hvmul0t 5004  hvsubidt 5005  hvm1negt 5007  hvadd12t 5012  hvadd4t 5013  hvsubcan2t 5017  hvsubsub4t 5032  his2subt 5052  normlem6 5068  normlem7t 5072  bcseq 5073  norm-iiit 5088  normpytht 5092  norm3adift 5098  hlim 5108  hlim2 5112  hlim0 5140  hlimcaui 5141  chocuni 5179  occllem2 5181  occllem3 5182  occllem5 5184  occllem6 5185  projlem7 5199  projlem22 5214  projlem23 5215  projlem25 5217  projlem26 5218  pjthlem7 5231  pjthlem8 5232  pjthlem9 5233  chdmm1t 5438  chdmm2t 5439  chjasst 5446  h1de2b 5459  elspansn2t 5472  spansncol 5473  spanunsn 5482  h1datom 5483  hosmvalt 5487  hodmvalt 5488  pjoml3t 5517  osumlem2 5531  5oalem2 5545  3oalem2 5553  pjadjt 5576  pjaddt 5577  pjsubt 5578  pjcjt2 5580  hosass 5607  pjadjco 5631  pjclem4 5653  pjadj2co 5656  pj3s 5659  pj3cor1 5661  pjopytht 5662  stjt 5676  strlem1 5691  strlem2 5692  strlem3a 5693  strlem4 5695  golem1 5704  mdbr3 5729  mdbr4 5730  dmdbr 5731  dmdi 5732  sumdmd 5787

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