Theorem opreq2i 3010

Description: Equality inference for operations.

Hypothesis

Ref	Expression
opreq1i.1	|- A = B

Assertion

Ref	Expression
opreq2i	|- (CFA) = (CFB)

Proof of Theorem opreq2i

Step	Hyp	Ref	Expression
1		opreq1i.1	. 2 |- A = B
2		opreq2 3007	. 2 |- (A = B -> (CFA) = (CFB))
3	1, 2	ax-mp 6	1 |- (CFA) = (CFB)

Syntax hints:   = wceq 1091  (class class class)co 3001

This theorem is referenced by:  opreq12i 3011  caopr32 3074  caopr4 3078  caopr42 3080  oa1suc 3132  om1 3144  oe1 3146  oawordeulem 3156  cdaassen 3725  addasspq 3857  mulidpq 3863  addclprlem2 3913  prlem934a 3931  prlem936a 3947  mulcmpblnrlem 3976  m1p1sr 3995  m1m1sr 3996  0idsr 4000  1idsr 4001  00sr 4002  pn0sr 4004  recexsrlem 4006  mulgt0sr 4008  sqgt0sr 4009  mappsrpr 4012  supsrlem2 4020  supsrlem5 4023  mulresr 4051  axmulcom 4071  axmulass 4073  axdistr 4074  ax0id 4076  ax1id 4077  axrecex 4079  axi2m1 4082  axcnre 4087  add42 4131  negid 4147  subneg 4148  negneg 4154  subeq0 4163  neg11 4164  muladd 4181  subdi 4182  mulzer1 4185  negdi2 4194  sub4 4206  divrec 4236  recrec 4253  rec11i 4261  ltsubadd 4316  ltneg 4330  ltmul1i 4393  2p2e4 4488  3p2e5 4492  3p3e6 4493  4p2e6 4494  4p3e7 4495  4p4e8 4496  5p2e7 4497  5p3e8 4498  5p4e9 4499  6p2e8 4500  6p3e9 4501  7p2e9 4502  3t3e9 4505  halfpost 4508  isqm1 4525  crulem 4528  crmult 4530  halfnz 4586  exp2t 4683  sqreci 4690  cu2 4711  binom 4712  discrlem1 4713  discrlem3 4715  nneo 4719  nnesq 4720  nn0opthlem1 4722  sqrlem2 4732  sqrlem11 4741  sqr2irrlem1 4777  cjcj 4808  recj 4812  imcj 4813  readd 4814  imadd 4815  cjmul 4819  ipcn 4820  cjmulrcl 4821  reneg 4824  imneg 4826  addcj 4828  absneg 4843  abscj 4844  absmul 4846  sqabsadd 4847  absid 4850  absre 4854  abstri 4859  abs3dif 4860  abslem2i 4866  ruclem1 4885  ruclem2 4886  ruclem15 4899  hvmul0t 5004  hvsubdistr1 5024  hvsubass 5027  hvsub23 5028  hvsubsub4 5031  hvnegdi 5034  hvsubeq0 5035  hvsubcan2 5036  hvsubadd 5038  hvsub0t 5041  normlem0 5062  normlem1 5063  normlem2 5064  normlem3 5065  normlem8 5071  norm-iii 5087  norm3dif 5094  normpar 5099  bcs 5101  occllem1 5180  projlem3 5195  projlem4 5196  projlem7 5199  pjthlem5 5229  pjthlem6 5230  pjthlem7 5231  pjthlem14 5238  chdmm3 5400  chdmm4 5401  chjidmt 5436  spanunsn 5482  pjoml4 5497  cmcm2 5502  qlax4 5523  qlax5 5524  pjadj 5564  pjmul 5568  pjsub 5569  pjssm 5572  pjcj 5575  hods0 5620  hosdass 5621  hosd2 5624  pjnel 5665  golem1 5704

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